author | immler@in.tum.de |
Wed, 10 Dec 2008 19:51:15 +0100 | |
changeset 34402 | bd8d70cd9baf |
parent 34401 | 44241a37b74a |
child 34407 | aad6834ba380 |
permissions | -rw-r--r-- |
34393 | 1 |
/* |
2 |
* RelativeAsset.scala |
|
3 |
* |
|
4 |
* To change this template, choose Tools | Template Manager |
|
5 |
* and open the template in the editor. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle.prover |
|
9 |
||
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
10 |
import sidekick.IAsset |
34393 | 11 |
import javax.swing._ |
12 |
import javax.swing.text.Position |
|
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
13 |
import javax.swing.tree._ |
34393 | 14 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
15 |
object MarkupNode { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
16 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
17 |
def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
18 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
19 |
class MyPos(val o : Int) extends Position { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
20 |
override def getOffset = o |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
21 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
22 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
23 |
implicit def int2pos(x : Int) : MyPos = new MyPos(x) |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
24 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
25 |
object RelativeAsset extends IAsset{ |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
26 |
override def getIcon : Icon = null |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
27 |
override def getShortString : String = node.short |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
28 |
override def getLongString : String = node.long |
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 getName : String = node.name |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
30 |
override def setName (name : String) = () |
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 setStart(start : Position) = () |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
32 |
override def getStart : Position = node.base.start + node.start |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
33 |
override def setEnd(end : Position) = () |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
34 |
override def getEnd : Position = node.base.start + node.end |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
35 |
override def toString = node.name + ": " + node.short |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
36 |
} |
34393 | 37 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
38 |
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
|
39 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
40 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
41 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
42 |
class MarkupNode (val base : Command, val start : Int, val end : Int, |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
43 |
val name : String, val short : String, val long : String) { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
44 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
45 |
val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this) |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
46 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
50 |
private var children_cell : List[MarkupNode] = Nil |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
51 |
//track changes in swing_node |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
52 |
def children = children_cell |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
53 |
def children_= (cs : List[MarkupNode]) = { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
54 |
swing_node.removeAllChildren |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
55 |
for(c <- cs) swing_node add c.swing_node |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
56 |
children_cell = cs |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
57 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
58 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
59 |
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
|
60 |
child parent = this |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
61 |
children_cell = (child :: children) sort ((a, b) => a.start < b.end) |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
62 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
63 |
swing_node add child.swing_node |
34393 | 64 |
} |
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 |
private def remove(nodes : 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 |
children_cell = children diff nodes |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
68 |
|
34402
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
69 |
for(node <- nodes) try { |
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
70 |
swing_node remove node.swing_node |
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
71 |
} catch { case e : IllegalArgumentException => |
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
72 |
System.err.println(e.toString) |
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
73 |
case e => throw e |
bd8d70cd9baf
information on command-phase left of scrollbar
immler@in.tum.de
parents:
34401
diff
changeset
|
74 |
} |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
75 |
} |
34393 | 76 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
77 |
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
|
78 |
var all = Nil : List[MarkupNode] |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
79 |
for(child <- children) |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
80 |
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
|
81 |
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
|
82 |
all |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
83 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
84 |
|
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
85 |
def insert(new_child : MarkupNode) : Unit = { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
86 |
if(new_child fitting_into this){ |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
87 |
for(child <- children){ |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
88 |
if(new_child fitting_into child) |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
89 |
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
|
90 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
91 |
if(new_child orphan){ |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
92 |
// 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
|
93 |
// -> insert new_child between this and its children |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
94 |
for(child <- children){ |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
95 |
if(child fitting_into new_child) { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
96 |
new_child add child |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
97 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
98 |
} |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
99 |
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
|
100 |
this remove new_child.children |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
101 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
102 |
} else { |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
103 |
System.err.println("ignored nonfitting markup " + new_child.name + new_child.short + new_child.long |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
104 |
+ "(" +new_child.start + ", "+ new_child.end + ")") |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
105 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
106 |
} |
34393 | 107 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
108 |
// 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
|
109 |
def fitting_into(node : MarkupNode) = node.start <= this.start && |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
110 |
node.end >= this.end |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
111 |
|
34393 | 112 |
} |