author | immler@in.tum.de |
Wed, 22 Apr 2009 17:35:49 +0200 | |
changeset 34554 | 7dc6c231da40 |
parent 34517 | 163cda249619 |
child 34555 | 7c001369956a |
permissions | -rw-r--r-- |
34393 | 1 |
/* |
34407 | 2 |
* Document markup nodes, with connection to Swing tree model |
34393 | 3 |
* |
34407 | 4 |
* @author Fabian Immler, TU Munich |
34393 | 5 |
*/ |
6 |
||
7 |
package isabelle.prover |
|
8 |
||
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
9 |
import isabelle.proofdocument.ProofDocument |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
10 |
|
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
11 |
import sidekick.IAsset |
34393 | 12 |
import javax.swing._ |
13 |
import javax.swing.text.Position |
|
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
14 |
import javax.swing.tree._ |
34393 | 15 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
16 |
object MarkupNode { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
17 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
18 |
def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = { |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
19 |
|
34480 | 20 |
implicit def int2pos(offset: Int): Position = |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
21 |
new Position { def getOffset = offset; override def toString = offset.toString} |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
22 |
|
34480 | 23 |
object RelativeAsset extends IAsset { |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
24 |
override def getIcon : Icon = null |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
25 |
override def getShortString : String = node.kind |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
26 |
override def getLongString : String = node.desc |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
27 |
override def getName : String = node.id |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
28 |
override def setName (name : String) = () |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
29 |
override def setStart(start : Position) = () |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
30 |
override def getStart : Position = node.abs_start(doc) |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
31 |
override def setEnd(end : Position) = () |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
32 |
override def getEnd : Position = node.abs_stop(doc) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
33 |
override def toString = node.id + ": " + node.kind + "[" + getStart + " - " + getEnd + "]" |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
34 |
} |
34393 | 35 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
36 |
new DefaultMutableTreeNode(RelativeAsset) |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
37 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
38 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
39 |
|
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
40 |
class MarkupNode (val base : Command, val start : Int, val stop : Int, |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
41 |
val id : String, val kind : String, val desc : String) { |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
42 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
43 |
def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = { |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
44 |
val node = MarkupNode.markup2default_node (this, base, doc) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
45 |
for (c <- children) node add c.swing_node(doc) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
46 |
node |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
47 |
} |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
48 |
|
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
49 |
def abs_start(doc: ProofDocument) = base.start(doc) + start |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
50 |
def abs_stop(doc: ProofDocument) = base.start(doc) + stop |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
51 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
52 |
var parent : MarkupNode = null |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
53 |
def orphan = parent == null |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
54 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
55 |
var children : List[MarkupNode] = Nil |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
56 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
57 |
private def add(child : MarkupNode) { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
58 |
child parent = this |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
59 |
children = (child :: children) sort ((a, b) => a.start < b.start) |
34393 | 60 |
} |
61 |
||
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
62 |
private def remove(nodes : List[MarkupNode]) { |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
63 |
children = children diff nodes |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
64 |
} |
34393 | 65 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
66 |
def dfs : List[MarkupNode] = { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
67 |
var all = Nil : List[MarkupNode] |
34503 | 68 |
for (child <- children) |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
69 |
all = child.dfs ::: all |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
70 |
all = this :: all |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
71 |
all |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
72 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
73 |
|
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
74 |
def leafs: List[MarkupNode] = { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
75 |
if (children == Nil) return List(this) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
76 |
else return children flatMap (_.leafs) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
77 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
78 |
|
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
79 |
def flatten: List[MarkupNode] = { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
80 |
var next_x = start |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
81 |
if(children.length == 0) List(this) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
82 |
else { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
83 |
val filled_gaps = for { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
84 |
child <- children |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
85 |
markups = if (next_x < child.start) { |
34517 | 86 |
new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
87 |
} else child.flatten |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
88 |
update = (next_x = child.stop) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
89 |
markup <- markups |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
90 |
} yield markup |
34517 | 91 |
if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, kind, "") |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
92 |
else filled_gaps |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
93 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
94 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
95 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
96 |
def insert(new_child : MarkupNode) : Unit = { |
34503 | 97 |
if (new_child fitting_into this) { |
98 |
for (child <- children) { |
|
99 |
if (new_child fitting_into child) |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
100 |
child insert new_child |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
101 |
} |
34503 | 102 |
if (new_child orphan) { |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
103 |
// new_child did not fit into children of this |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
104 |
// -> insert new_child between this and its children |
34503 | 105 |
for (child <- children) { |
106 |
if (child fitting_into new_child) { |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
107 |
new_child add child |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
108 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
109 |
} |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
110 |
this add new_child |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
111 |
this remove new_child.children |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
112 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
113 |
} else { |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
114 |
System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
115 |
+ "(" +new_child.start + ", "+ new_child.stop + ")") |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
116 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
117 |
} |
34393 | 118 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
119 |
// does this fit into node? |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
120 |
def fitting_into(node : MarkupNode) = node.start <= this.start && |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
121 |
node.stop >= this.stop |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
122 |
|
34517 | 123 |
override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc |
34393 | 124 |
} |