|
1 /* Title: Pure/PIDE/markup_tree.scala |
|
2 Author: Fabian Immler, TU Munich |
|
3 Author: Makarius |
|
4 |
|
5 Markup trees over nested / non-overlapping text ranges. |
|
6 */ |
|
7 |
|
8 package isabelle |
|
9 |
|
10 |
|
11 import javax.swing.tree.DefaultMutableTreeNode |
|
12 |
|
13 import scala.collection.immutable.SortedMap |
|
14 import scala.collection.mutable |
|
15 import scala.annotation.tailrec |
|
16 |
|
17 |
|
18 object Markup_Tree |
|
19 { |
|
20 case class Node(val range: Text.Range, val info: Any) |
|
21 |
|
22 |
|
23 /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */ |
|
24 |
|
25 object Branches |
|
26 { |
|
27 type Entry = (Node, Markup_Tree) |
|
28 type T = SortedMap[Node, Entry] |
|
29 |
|
30 val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node] |
|
31 { |
|
32 def compare(x: Node, y: Node): Int = x.range compare y.range |
|
33 }) |
|
34 def update(branches: T, entries: Entry*): T = |
|
35 branches ++ entries.map(e => (e._1 -> e)) |
|
36 def make(entries: List[Entry]): T = update(empty, entries:_*) |
|
37 } |
|
38 |
|
39 val empty = new Markup_Tree(Branches.empty) |
|
40 } |
|
41 |
|
42 |
|
43 case class Markup_Tree(val branches: Markup_Tree.Branches.T) |
|
44 { |
|
45 import Markup_Tree._ |
|
46 |
|
47 def + (new_node: Node): Markup_Tree = |
|
48 { |
|
49 // FIXME tune overlapping == branches && rest.isEmpty |
|
50 val (overlapping, rest) = |
|
51 { |
|
52 val overlapping = new mutable.ListBuffer[Branches.Entry] |
|
53 var rest = branches |
|
54 while (rest.isDefinedAt(new_node)) { |
|
55 overlapping += rest(new_node) |
|
56 rest -= new_node |
|
57 } |
|
58 (overlapping.toList, rest) |
|
59 } |
|
60 overlapping match { |
|
61 case Nil => |
|
62 new Markup_Tree(Branches.update(branches, new_node -> empty)) |
|
63 |
|
64 case List((node, subtree)) |
|
65 if node.range != new_node.range && (node.range contains new_node.range) => |
|
66 new Markup_Tree(Branches.update(branches, node -> (subtree + new_node))) |
|
67 |
|
68 case _ if overlapping.forall(e => new_node.range contains e._1.range) => |
|
69 val new_tree = new Markup_Tree(Branches.make(overlapping)) |
|
70 new Markup_Tree(Branches.update(rest, new_node -> new_tree)) |
|
71 |
|
72 case _ => // FIXME split markup!? |
|
73 System.err.println("Ignored overlapping markup: " + new_node); this |
|
74 } |
|
75 } |
|
76 |
|
77 // FIXME depth-first with result markup stack |
|
78 // FIXME projection to given range |
|
79 def flatten(parent: Node): List[Node] = |
|
80 { |
|
81 val result = new mutable.ListBuffer[Node] |
|
82 var offset = parent.range.start |
|
83 for ((_, (node, subtree)) <- branches.iterator) { |
|
84 if (offset < node.range.start) |
|
85 result += new Node(Text.Range(offset, node.range.start), parent.info) |
|
86 result ++= subtree.flatten(node) |
|
87 offset = node.range.stop |
|
88 } |
|
89 if (offset < parent.range.stop) |
|
90 result += new Node(Text.Range(offset, parent.range.stop), parent.info) |
|
91 result.toList |
|
92 } |
|
93 |
|
94 def filter(pred: Node => Boolean): Markup_Tree = |
|
95 { |
|
96 val bs = branches.toList.flatMap(entry => { |
|
97 val (_, (node, subtree)) = entry |
|
98 if (pred(node)) List((node, (node, subtree.filter(pred)))) |
|
99 else subtree.filter(pred).branches.toList |
|
100 }) |
|
101 new Markup_Tree(Branches.empty ++ bs) |
|
102 } |
|
103 |
|
104 def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode) |
|
105 { |
|
106 for ((_, (node, subtree)) <- branches) { |
|
107 val current = swing_node(node) |
|
108 subtree.swing_tree(current)(swing_node) |
|
109 parent.add(current) |
|
110 } |
|
111 } |
|
112 } |
|
113 |