author | wenzelm |
Tue, 02 Jun 2009 21:20:22 +0200 | |
changeset 34582 | 5d5d253c7c29 |
parent 34577 | aef72e071725 |
child 34597 | a0c84b0edb9a |
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 |
|
34564
850dc36d4926
let MarkupNode carry arbitrary information
immler@in.tum.de
parents:
34561
diff
changeset
|
16 |
abstract class MarkupInfo |
34577 | 17 |
case class RootInfo() extends MarkupInfo |
34582 | 18 |
case class OuterInfo(highlight: String) extends |
19 |
MarkupInfo { override def toString = highlight } |
|
20 |
case class HighlightInfo(highlight: String) extends |
|
21 |
MarkupInfo { override def toString = highlight } |
|
22 |
case class TypeInfo(type_kind: String) extends |
|
23 |
MarkupInfo { override def toString = type_kind } |
|
34568
b517d0607297
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@in.tum.de
parents:
34564
diff
changeset
|
24 |
case class RefInfo(file: Option[String], line: Option[Int], |
34582 | 25 |
command_id: Option[String], offset: Option[Int]) extends MarkupInfo { |
26 |
override def toString = (file, line, command_id, offset).toString |
|
27 |
} |
|
34564
850dc36d4926
let MarkupNode carry arbitrary information
immler@in.tum.de
parents:
34561
diff
changeset
|
28 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
29 |
object MarkupNode { |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
30 |
|
34582 | 31 |
def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) |
32 |
: DefaultMutableTreeNode = { |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
33 |
|
34480 | 34 |
implicit def int2pos(offset: Int): Position = |
34582 | 35 |
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
|
36 |
|
34480 | 37 |
object RelativeAsset extends IAsset { |
34582 | 38 |
override def getIcon: Icon = null |
39 |
override def getShortString: String = node.content |
|
40 |
override def getLongString: String = node.info.toString |
|
41 |
override def getName: String = node.id |
|
42 |
override def setName(name: String) = () |
|
43 |
override def setStart(start: Position) = () |
|
44 |
override def getStart: Position = node.abs_start(doc) |
|
45 |
override def setEnd(end: Position) = () |
|
46 |
override def getEnd: Position = node.abs_stop(doc) |
|
34555
7c001369956a
included information on ML status messages in Sidekick's status-window
immler@in.tum.de
parents:
34554
diff
changeset
|
47 |
override def toString = node.id + ": " + node.content + "[" + 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
|
48 |
} |
34393 | 49 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
50 |
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
|
51 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
52 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
53 |
|
34582 | 54 |
class MarkupNode(val base: Command, val start: Int, val stop: Int, |
55 |
val children: List[MarkupNode], |
|
56 |
val id: String, val content: String, val info: MarkupInfo) |
|
57 |
{ |
|
58 |
def swing_node(doc: ProofDocument): DefaultMutableTreeNode = { |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
59 |
val node = MarkupNode.markup2default_node (this, base, doc) |
34557 | 60 |
children.map(node add _.swing_node(doc)) |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
61 |
node |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
62 |
} |
34557 | 63 |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34517
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
|
34557 | 67 |
def set_children(newchildren: List[MarkupNode]): MarkupNode = |
34564
850dc36d4926
let MarkupNode carry arbitrary information
immler@in.tum.de
parents:
34561
diff
changeset
|
68 |
new MarkupNode(base, start, stop, newchildren, id, content, info) |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
69 |
|
34582 | 70 |
def add(child: MarkupNode) = |
71 |
set_children ((child :: children) sort ((a, b) => a.start < b.start)) |
|
34393 | 72 |
|
34582 | 73 |
def remove(nodes: List[MarkupNode]) = set_children(children diff nodes) |
34393 | 74 |
|
34582 | 75 |
def dfs: List[MarkupNode] = { |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
76 |
var all = Nil : List[MarkupNode] |
34503 | 77 |
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
|
78 |
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
|
79 |
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
|
80 |
all |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
81 |
} |
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
82 |
|
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
83 |
def leafs: List[MarkupNode] = { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
84 |
if (children == Nil) return List(this) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
85 |
else return children flatMap (_.leafs) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
86 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
87 |
|
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
88 |
def flatten: List[MarkupNode] = { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
89 |
var next_x = start |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
90 |
if(children.length == 0) List(this) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
91 |
else { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
92 |
val filled_gaps = for { |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
93 |
child <- children |
34582 | 94 |
markups = |
95 |
if (next_x < child.start) { |
|
96 |
new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: child.flatten |
|
97 |
} else child.flatten |
|
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
98 |
update = (next_x = child.stop) |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
99 |
markup <- markups |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
100 |
} yield markup |
34582 | 101 |
if (next_x < stop) |
102 |
filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info) |
|
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
103 |
else filled_gaps |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
104 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
105 |
} |
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
106 |
|
34582 | 107 |
def filter(p: MarkupNode => Boolean): List[MarkupNode] = { |
34559 | 108 |
val filtered = children.flatMap(_.filter(p)) |
109 |
if (p(this)) List(this set_children(filtered)) |
|
110 |
else filtered |
|
111 |
} |
|
112 |
||
34582 | 113 |
def +(new_child: MarkupNode): MarkupNode = { |
34503 | 114 |
if (new_child fitting_into this) { |
34561 | 115 |
var inserted = false |
34582 | 116 |
val new_children = |
117 |
children.map(c => |
|
118 |
if ((new_child fitting_into c) && !inserted) {inserted = true; c + new_child} |
|
119 |
else c) |
|
34561 | 120 |
if (!inserted) { |
34582 | 121 |
// new_child did not fit into children of this |
122 |
// -> insert new_child between this and its children |
|
34561 | 123 |
val fitting = children filter(_ fitting_into new_child) |
124 |
(this remove fitting) add ((new_child /: fitting) (_ + _)) |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
125 |
} |
34557 | 126 |
else this set_children new_children |
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
127 |
} else { |
34582 | 128 |
error("ignored nonfitting markup " + new_child.id + new_child.content + |
129 |
new_child.info.toString + "(" +new_child.start + ", "+ new_child.stop + ")") |
|
34400
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
130 |
} |
1b61a92f8675
MarkupNode instead of DefaultMutableTreeNode and RelativeAsset
immler@in.tum.de
parents:
34393
diff
changeset
|
131 |
} |
34393 | 132 |
|
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34400
diff
changeset
|
133 |
// does this fit into node? |
34582 | 134 |
def fitting_into(node: MarkupNode) = node.start <= this.start && node.stop >= this.stop |
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset
|
135 |
|
34582 | 136 |
override def toString = |
137 |
"([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString |
|
34393 | 138 |
} |