# HG changeset patch # User wenzelm # Date 1282251120 -7200 # Node ID a6e2715fac5f535cf54457263d2841ed4e46c453 # Parent f6c9a4f9f66f60c2b8cc790065aed2817e61679d parameterized type Markup_Tree.Node; Markup_Tree.select: allow arbitrary interpretations, not just filtering; renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps; diff -r f6c9a4f9f66f -r a6e2715fac5f src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Aug 19 22:26:15 2010 +0200 +++ b/src/Pure/PIDE/command.scala Thu Aug 19 22:52:00 2010 +0200 @@ -37,16 +37,16 @@ def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) - def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node) + def add_markup(node: Markup_Tree.Node[Any]): State = copy(markup = markup + node) - def markup_root_node: Markup_Tree.Node = + def markup_root_node: Markup_Tree.Node[Any] = new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status)) def markup_root: Markup_Tree = markup + markup_root_node /* markup */ - lazy val highlight: List[Markup_Tree.Node] = + lazy val highlight: List[Markup_Tree.Node[Any]] = { markup.filter(_.info match { case Command.HighlightInfo(_, _) => true @@ -54,7 +54,7 @@ }).flatten(markup_root_node) } - private lazy val types: List[Markup_Tree.Node] = + private lazy val types: List[Markup_Tree.Node[Any]] = markup.filter(_.info match { case Command.TypeInfo(_) => true case _ => false }).flatten(markup_root_node) @@ -71,12 +71,12 @@ } } - private lazy val refs: List[Markup_Tree.Node] = + private lazy val refs: List[Markup_Tree.Node[Any]] = markup.filter(_.info match { case Command.RefInfo(_, _, _, _) => true case _ => false }).flatten(markup_root_node) - def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] = + def ref_at(pos: Text.Offset): Option[Markup_Tree.Node[Any]] = refs.find(_.range.contains(pos)) @@ -159,7 +159,7 @@ /* markup */ - def decode_range(range: Text.Range, info: Any): Markup_Tree.Node = + def decode_range(range: Text.Range, info: Any): Markup_Tree.Node[Any] = new Markup_Tree.Node(symbol_index.decode(range), info) diff -r f6c9a4f9f66f -r a6e2715fac5f src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Thu Aug 19 22:26:15 2010 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Thu Aug 19 22:52:00 2010 +0200 @@ -17,10 +17,10 @@ object Markup_Tree { - case class Node(val range: Text.Range, val info: Any) + case class Node[A](val range: Text.Range, val info: A) { - def contains(that: Node): Boolean = this.range contains that.range - def restrict(r: Text.Range): Node = Node(range.intersect(r), info) + def contains[B](that: Node[B]): Boolean = this.range contains that.range + def restrict(r: Text.Range): Node[A] = Node(range.restrict(r), info) } @@ -28,12 +28,12 @@ object Branches { - type Entry = (Node, Markup_Tree) - type T = SortedMap[Node, Entry] + type Entry = (Node[Any], Markup_Tree) + type T = SortedMap[Node[Any], Entry] - val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node] + val empty = SortedMap.empty[Node[Any], Entry](new scala.math.Ordering[Node[Any]] { - def compare(x: Node, y: Node): Int = x.range compare y.range + def compare(x: Node[Any], y: Node[Any]): Int = x.range compare y.range }) def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry) @@ -56,7 +56,7 @@ case list => list.mkString("Tree(", ",", ")") } - def + (new_node: Node): Markup_Tree = + def + (new_node: Node[Any]): Markup_Tree = { branches.get(new_node) match { case None => @@ -82,9 +82,9 @@ // FIXME depth-first with result markup stack // FIXME projection to given range - def flatten(parent: Node): List[Node] = + def flatten(parent: Node[Any]): List[Node[Any]] = { - val result = new mutable.ListBuffer[Node] + val result = new mutable.ListBuffer[Node[Any]] var offset = parent.range.start for ((_, (node, subtree)) <- branches.iterator) { if (offset < node.range.start) @@ -97,7 +97,7 @@ result.toList } - def filter(pred: Node => Boolean): Markup_Tree = + def filter(pred: Node[Any] => Boolean): Markup_Tree = { val bs = branches.toList.flatMap(entry => { val (_, (node, subtree)) = entry @@ -107,24 +107,26 @@ new Markup_Tree(Branches.empty ++ bs) } - def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] = + def select[A](range: Text.Range)(sel: PartialFunction[Any, A]): Stream[Node[List[A]]] = { - def stream(parent: Node, bs: Branches.T): Stream[Node] = + def stream(parent: Node[List[A]], bs: Branches.T): Stream[Node[List[A]]] = { val substream = (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield { - if (sel.isDefinedAt(node)) - stream(node.restrict(parent.range), subtree.branches) + if (sel.isDefinedAt(node.info)) { + val current = Node(node.range.restrict(parent.range), List(sel(node.info))) + stream(current, subtree.branches) + } else stream(parent, subtree.branches) }).flatten - def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] = + def padding(last: Text.Offset, s: Stream[Node[List[A]]]): Stream[Node[List[A]]] = s match { case (node @ Node(Text.Range(start, stop), _)) #:: rest => if (last < start) parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest) else node #:: padding(stop, rest) - case Stream.Empty => // FIXME + case Stream.Empty => if (last < parent.range.stop) Stream(parent.restrict(Text.Range(last, parent.range.stop))) else Stream.Empty @@ -134,7 +136,7 @@ stream(Node(range, Nil), branches) } - def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode) + def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode) { for ((_, (node, subtree)) <- branches) { val current = swing_node(node) diff -r f6c9a4f9f66f -r a6e2715fac5f src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Thu Aug 19 22:26:15 2010 +0200 +++ b/src/Pure/PIDE/text.scala Thu Aug 19 22:52:00 2010 +0200 @@ -38,7 +38,7 @@ def start_range: Range = Range(start, start) def stop_range: Range = Range(stop, stop) - def intersect(that: Range): Range = + def restrict(that: Range): Range = Range(this.start max that.start, this.stop min that.stop) } diff -r f6c9a4f9f66f -r a6e2715fac5f src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 19 22:26:15 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 19 22:52:00 2010 +0200 @@ -129,7 +129,7 @@ val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) { - snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) => + snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node[Any]) => { val content = command.source(node.range).replace('\n', ' ') val id = command.id