+def revert_amsmath(document):
+ " Revert \\use_amsmath"
+ i = find_token(document.header, "\\use_amsmath", 0)
+ if i == -1:
+ document.warning("Malformed LyX document: Missing '\\use_amsmath'.")
+ return
+ tokens = document.header[i].split()
+ if len(tokens) != 2:
+ document.warning("Malformed LyX document: Could not parse line '%s'." % document.header[i])
+ use_amsmath = '0'
+ else:
+ use_amsmath = tokens[1]
+ # old: 0 == off, 1 == on
+ # new: 0 == off, 1 == auto, 2 == on
+ # translate auto -> off, since old format 'off' means auto in reality
+ if use_amsmath == '2':
+ document.header[i] = "\\use_amsmath 1"
+ else:
+ document.header[i] = "\\use_amsmath 0"
+
+
+def convert_spaces(document):
+ " \SpecialChar ~ -> \InsetSpace ~"
+ for i in range(len(document.body)):
+ document.body[i] = document.body[i].replace("\\SpecialChar ~",
+ "\\InsetSpace ~")
+
+
+def revert_spaces(document):
+ " \InsetSpace ~ -> \SpecialChar ~"
+ regexp = re.compile(r'(.*)(\\InsetSpace\s+)(\S+)')
+ i = 0
+ while 1:
+ i = find_re(document.body, regexp, i)
+ if i == -1:
+ break
+ space = regexp.match(document.body[i]).group(3)
+ prepend = regexp.match(document.body[i]).group(1)
+ if space == '~':
+ document.body[i] = regexp.sub(prepend + '\\SpecialChar ~', document.body[i])
+ i = i + 1
+ else:
+ document.body[i] = regexp.sub(prepend, document.body[i])
+ document.body[i+1:i+1] = ''
+ if space == "\\space":
+ space = "\\ "
+ i = insert_ert(document.body, i+1, 'Collapsed', space, document.format - 1, document.default_layout)
+
+
+def rename_spaces(document):
+ """ \InsetSpace \, -> \InsetSpace \thinspace{}
+ \InsetSpace \space -> \InsetSpace \space{}"""
+ for i in range(len(document.body)):
+ document.body[i] = document.body[i].replace("\\InsetSpace \\space",
+ "\\InsetSpace \\space{}")
+ document.body[i] = document.body[i].replace("\\InsetSpace \,",
+ "\\InsetSpace \\thinspace{}")
+
+
+def revert_space_names(document):
+ """ \InsetSpace \thinspace{} -> \InsetSpace \,
+ \InsetSpace \space{} -> \InsetSpace \space"""
+ for i in range(len(document.body)):
+ document.body[i] = document.body[i].replace("\\InsetSpace \\space{}",
+ "\\InsetSpace \\space")
+ document.body[i] = document.body[i].replace("\\InsetSpace \\thinspace{}",
+ "\\InsetSpace \\,")