36 new DefaultMutableTreeNode(RelativeAsset) |
36 new DefaultMutableTreeNode(RelativeAsset) |
37 } |
37 } |
38 } |
38 } |
39 |
39 |
40 class MarkupNode (val base : Command, val start : Int, val stop : Int, |
40 class MarkupNode (val base : Command, val start : Int, val stop : Int, |
41 val id : String, val content : String, val desc : String) { |
41 val children: List[MarkupNode], |
|
42 val id : String, val content : String, val desc : String) { |
42 |
43 |
43 def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { |
44 def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { |
44 val node = MarkupNode.markup2default_node (this, base, doc) |
45 val node = MarkupNode.markup2default_node (this, base, doc) |
45 for (c <- children) node add c.swing_node(doc) |
46 children.map(node add _.swing_node(doc)) |
46 node |
47 node |
47 } |
48 } |
48 |
49 |
49 def abs_start(doc: ProofDocument) = base.start(doc) + start |
50 def abs_start(doc: ProofDocument) = base.start(doc) + start |
50 def abs_stop(doc: ProofDocument) = base.start(doc) + stop |
51 def abs_stop(doc: ProofDocument) = base.start(doc) + stop |
51 |
52 |
52 var parent : MarkupNode = null |
53 def set_children(newchildren: List[MarkupNode]): MarkupNode = |
53 def orphan = parent == null |
54 new MarkupNode(base, start, stop, newchildren, id, content, desc) |
54 |
55 |
55 var children : List[MarkupNode] = Nil |
56 def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start)) |
56 |
57 |
57 private def add(child : MarkupNode) { |
58 def remove(nodes : List[MarkupNode]) = set_children(children diff nodes) |
58 child parent = this |
|
59 children = (child :: children) sort ((a, b) => a.start < b.start) |
|
60 } |
|
61 |
|
62 private def remove(nodes : List[MarkupNode]) { |
|
63 children = children diff nodes |
|
64 } |
|
65 |
59 |
66 def dfs : List[MarkupNode] = { |
60 def dfs : List[MarkupNode] = { |
67 var all = Nil : List[MarkupNode] |
61 var all = Nil : List[MarkupNode] |
68 for (child <- children) |
62 for (child <- children) |
69 all = child.dfs ::: all |
63 all = child.dfs ::: all |
81 if(children.length == 0) List(this) |
75 if(children.length == 0) List(this) |
82 else { |
76 else { |
83 val filled_gaps = for { |
77 val filled_gaps = for { |
84 child <- children |
78 child <- children |
85 markups = if (next_x < child.start) { |
79 markups = if (next_x < child.start) { |
86 new MarkupNode(base, next_x, child.start, id, content, "") :: child.flatten |
80 new MarkupNode(base, next_x, child.start, Nil, id, content, "") :: child.flatten |
87 } else child.flatten |
81 } else child.flatten |
88 update = (next_x = child.stop) |
82 update = (next_x = child.stop) |
89 markup <- markups |
83 markup <- markups |
90 } yield markup |
84 } yield markup |
91 if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, content, "") |
85 if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, "") |
92 else filled_gaps |
86 else filled_gaps |
93 } |
87 } |
94 } |
88 } |
95 |
89 |
96 def insert(new_child : MarkupNode) : Unit = { |
90 def +(new_child : MarkupNode) : MarkupNode = { |
97 if (new_child fitting_into this) { |
91 if (new_child fitting_into this) { |
98 for (child <- children) { |
92 val new_children = children.map(c => if((new_child fitting_into c)) c + new_child else c) |
99 if (new_child fitting_into child) |
93 if (new_children == children) { |
100 child insert new_child |
94 // new_child did not fit into children of this -> insert new_child between this and its children |
|
95 val (fitting, nonfitting) = children span(_ fitting_into new_child) |
|
96 this remove fitting add ((new_child /: fitting) (_ add _)) |
101 } |
97 } |
102 if (new_child orphan) { |
98 else this set_children new_children |
103 // new_child did not fit into children of this |
|
104 // -> insert new_child between this and its children |
|
105 for (child <- children) { |
|
106 if (child fitting_into new_child) { |
|
107 new_child add child |
|
108 } |
|
109 } |
|
110 this add new_child |
|
111 this remove new_child.children |
|
112 } |
|
113 } else { |
99 } else { |
114 System.err.println("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc |
100 error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc |
115 + "(" +new_child.start + ", "+ new_child.stop + ")") |
101 + "(" +new_child.start + ", "+ new_child.stop + ")") |
116 } |
102 } |
117 } |
103 } |
118 |
104 |
119 // does this fit into node? |
105 // does this fit into node? |
120 def fitting_into(node : MarkupNode) = node.start <= this.start && |
106 def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop |
121 node.stop >= this.stop |
|
122 |
107 |
123 override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc |
108 override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc |
124 } |
109 } |