author  wenzelm 
Thu, 19 Aug 2010 12:41:40 +0200  
changeset 38482  7b6ee937b75f 
parent 38479  e628da370072 
child 38486  f5bbfc019937 
permissions  rwrr 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

1 
/* Title: Pure/PIDE/markup_tree.scala 
36676  2 
Author: Fabian Immler, TU Munich 
3 
Author: Makarius 

4 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

5 
Markup trees over nested / nonoverlapping text ranges. 
36676  6 
*/ 
34393  7 

34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar  except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34760
diff
changeset

8 
package isabelle 
34393  9 

34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset

10 

80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset

11 
import javax.swing.tree.DefaultMutableTreeNode 
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34676
diff
changeset

12 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

13 
import scala.collection.immutable.SortedMap 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

14 
import scala.collection.mutable 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

15 
import scala.annotation.tailrec 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

16 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

17 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

18 
object Markup_Tree 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

19 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

20 
case class Node(val range: Text.Range, val info: Any) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

21 
{ 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

22 
def contains(that: Node): Boolean = this.range contains that.range 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

23 
} 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

24 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

25 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

26 
/* branches sorted by quasiorder  overlapping intervals appear as equivalent */ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

27 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

28 
object Branches 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

29 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

30 
type Entry = (Node, Markup_Tree) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

31 
type T = SortedMap[Node, Entry] 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

32 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

33 
val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node] 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

34 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

35 
def compare(x: Node, y: Node): Int = x.range compare y.range 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

36 
}) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

37 
def update(branches: T, entries: Entry*): T = 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

38 
branches ++ entries.map(e => (e._1 > e)) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

39 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

40 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

41 
val empty = new Markup_Tree(Branches.empty) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

42 
} 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34517
diff
changeset

43 

34393  44 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

45 
case class Markup_Tree(val branches: Markup_Tree.Branches.T) 
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset

46 
{ 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

47 
import Markup_Tree._ 
34557  48 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

49 
def + (new_node: Node): Markup_Tree = 
34703  50 
{ 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

51 
branches.get(new_node) match { 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

52 
case None => 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

53 
new Markup_Tree(Branches.update(branches, new_node > empty)) 
38482
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

54 
case Some((node, subtree)) => 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

55 
if (node.range != new_node.range && node.contains(new_node)) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

56 
new Markup_Tree(Branches.update(branches, node > (subtree + new_node))) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

57 
else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1)) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

58 
new Markup_Tree(Branches.update(Branches.empty, (new_node > this))) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

59 
else { 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

60 
var overlapping = Branches.empty 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

61 
var rest = branches 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

62 
while (rest.isDefinedAt(new_node)) { 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

63 
overlapping = Branches.update(overlapping, rest(new_node)) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

64 
rest = new_node 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

65 
} 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

66 
if (overlapping.forall(e => new_node.contains(e._1))) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

67 
new Markup_Tree(Branches.update(rest, new_node > new Markup_Tree(overlapping))) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

68 
else { // FIXME split markup!? 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

69 
System.err.println("Ignored overlapping markup: " + new_node) 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

70 
this 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

71 
} 
7b6ee937b75f
tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents:
38479
diff
changeset

72 
} 
34703  73 
} 
74 
} 

75 

38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

76 
// FIXME depthfirst with result markup stack 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

77 
// FIXME projection to given range 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

78 
def flatten(parent: Node): List[Node] = 
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset

79 
{ 
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

80 
val result = new mutable.ListBuffer[Node] 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

81 
var offset = parent.range.start 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

82 
for ((_, (node, subtree)) < branches.iterator) { 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

83 
if (offset < node.range.start) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

84 
result += new Node(Text.Range(offset, node.range.start), parent.info) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

85 
result ++= subtree.flatten(node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

86 
offset = node.range.stop 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

87 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

88 
if (offset < parent.range.stop) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

89 
result += new Node(Text.Range(offset, parent.range.stop), parent.info) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

90 
result.toList 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

91 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

92 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

93 
def filter(pred: Node => Boolean): Markup_Tree = 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

94 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

95 
val bs = branches.toList.flatMap(entry => { 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

96 
val (_, (node, subtree)) = entry 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

97 
if (pred(node)) List((node, (node, subtree.filter(pred)))) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

98 
else subtree.filter(pred).branches.toList 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

99 
}) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

100 
new Markup_Tree(Branches.empty ++ bs) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

101 
} 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

102 

e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

103 
def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

104 
{ 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

105 
for ((_, (node, subtree)) < branches) { 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

106 
val current = swing_node(node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

107 
subtree.swing_tree(current)(swing_node) 
e628da370072
more efficient Markup_Tree, based on branches sorted by quasiorder;
wenzelm
parents:
38478
diff
changeset

108 
parent.add(current) 
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset

109 
} 
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset

110 
} 
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset

111 
} 
34514
2104a836b415
renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents:
34503
diff
changeset

112 