equal
deleted
inserted
replaced
69 def abs_stop(doc: ProofDocument) = base.start(doc) + stop |
69 def abs_stop(doc: ProofDocument) = base.start(doc) + stop |
70 |
70 |
71 def set_children(newchildren: List[MarkupNode]): MarkupNode = |
71 def set_children(newchildren: List[MarkupNode]): MarkupNode = |
72 new MarkupNode(base, start, stop, newchildren, id, content, info) |
72 new MarkupNode(base, start, stop, newchildren, id, content, info) |
73 |
73 |
74 def add(child: MarkupNode) = |
74 private def add(child: MarkupNode) = |
75 set_children ((child :: children) sort ((a, b) => a.start < b.start)) |
75 set_children ((child :: children) sort ((a, b) => a.start < b.start)) |
76 |
76 |
77 def remove(nodes: List[MarkupNode]) = set_children(children diff nodes) |
77 def remove(nodes: List[MarkupNode]) = set_children(children diff nodes) |
78 |
78 |
79 def dfs: List[MarkupNode] = { |
79 def dfs: List[MarkupNode] = { |