equal
deleted
inserted
replaced
66 |
66 |
67 |
67 |
68 /* result structure */ |
68 /* result structure */ |
69 |
69 |
70 val spans = parse_spans(syntax.scan(text)) |
70 val spans = parse_spans(syntax.scan(text)) |
71 spans.foreach(span => add(Command(Document.no_id, node_name, span))) |
71 spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty))) |
72 result() |
72 result() |
73 } |
73 } |
74 } |
74 } |
75 |
75 |
76 |
76 |
224 case Nil => |
224 case Nil => |
225 assert(spans2.isEmpty) |
225 assert(spans2.isEmpty) |
226 commands |
226 commands |
227 case cmd :: _ => |
227 case cmd :: _ => |
228 val hook = commands.prev(cmd) |
228 val hook = commands.prev(cmd) |
229 val inserted = spans2.map(span => Command(Document.new_id(), name, span)) |
229 val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty)) |
230 (commands /: cmds2)(_ - _).append_after(hook, inserted) |
230 (commands /: cmds2)(_ - _).append_after(hook, inserted) |
231 } |
231 } |
232 } |
232 } |
233 |
233 |
234 |
234 |