def convert_spaceinset(document):
" Convert '\\InsetSpace foo' to '\\begin_inset Space foo\n\\end_inset' "
for i in range(len(document.body)):
- if re.search(r'\InsetSpace', document.body[i]):
- document.body[i] = document.body[i].replace('\\InsetSpace', '\n\\begin_inset Space')
- document.body[i] = document.body[i] + "\n\\end_inset"
+ m = re.match(r'(.*)\\InsetSpace (.*)', document.body[i])
+ if m:
+ before = m.group(1)
+ after = m.group(2)
+ subst = [before, "\\begin_inset Space " + after, "\\end_inset"]
+ document.body[i: i+1] = subst
def revert_spaceinset(document):