# HG changeset patch # User wenzelm # Date 1282167890 -7200 # Node ID e628da370072599a9c4c8c37a2f5f8ab8851133b # Parent 7766812a01e775737b8d38b4d7a97a720f33c89b more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned; diff -r 7766812a01e7 -r e628da370072 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Aug 18 14:04:13 2010 +0200 +++ b/src/Pure/General/position.scala Wed Aug 18 23:44:50 2010 +0200 @@ -20,13 +20,13 @@ def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos) def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos) - def get_range(pos: T): Option[(Int, Int)] = + def get_range(pos: T): Option[Text.Range] = (get_offset(pos), get_end_offset(pos)) match { - case (Some(begin), Some(end)) => Some(begin, end) - case (Some(begin), None) => Some(begin, begin + 1) + case (Some(start), Some(stop)) => Some(Text.Range(start, stop)) + case (Some(start), None) => Some(Text.Range(start, start + 1)) case (None, _) => None } object Id { def unapply(pos: T): Option[Long] = get_id(pos) } - object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) } + object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) } } diff -r 7766812a01e7 -r e628da370072 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Aug 18 14:04:13 2010 +0200 +++ b/src/Pure/General/symbol.scala Wed Aug 18 23:44:50 2010 +0200 @@ -106,8 +106,9 @@ } buf.toArray } - def decode(sym: Int): Int = + def decode(sym1: Int): Int = { + val sym = sym1 - 1 val end = index.length def bisect(a: Int, b: Int): Int = { @@ -123,6 +124,7 @@ if (i < 0) sym else index(i).chr + sym - index(i).sym } + def decode(range: Text.Range): Text.Range = range.map(decode(_)) } diff -r 7766812a01e7 -r e628da370072 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Aug 18 14:04:13 2010 +0200 +++ b/src/Pure/PIDE/command.scala Wed Aug 18 23:44:50 2010 +0200 @@ -29,7 +29,7 @@ val command: Command, val status: List[Markup], val reverse_results: List[XML.Tree], - val markup: Markup_Text) + val markup: Markup_Tree) { /* content */ @@ -37,23 +37,26 @@ def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) - def add_markup(node: Markup_Tree): State = copy(markup = markup + node) + def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node) + + def markup_root_node: Markup_Tree.Node = new Markup_Tree.Node(command.range, status) + def markup_root: Markup_Tree = markup + markup_root_node /* markup */ - lazy val highlight: Markup_Text = + lazy val highlight: List[Markup_Tree.Node] = { markup.filter(_.info match { case Command.HighlightInfo(_, _) => true case _ => false - }) + }).flatten(markup_root_node) } - private lazy val types: List[Markup_Node] = + private lazy val types: List[Markup_Tree.Node] = markup.filter(_.info match { case Command.TypeInfo(_) => true - case _ => false }).flatten + case _ => false }).flatten(markup_root_node) def type_at(pos: Text.Offset): Option[String] = { @@ -67,12 +70,12 @@ } } - private lazy val refs: List[Markup_Node] = + private lazy val refs: List[Markup_Tree.Node] = markup.filter(_.info match { case Command.RefInfo(_, _, _, _) => true - case _ => false }).flatten + case _ => false }).flatten(markup_root_node) - def ref_at(pos: Text.Offset): Option[Markup_Node] = + def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] = refs.find(_.range.contains(pos)) @@ -88,18 +91,16 @@ elem match { case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => atts match { - case Position.Range(begin, end) => + case Position.Range(range) => if (kind == Markup.ML_TYPING) { val info = Pretty.string_of(body, margin = 40) - state.add_markup( - command.markup_node(begin, end, Command.TypeInfo(info))) + state.add_markup(command.decode_range(range, Command.TypeInfo(info))) } else if (kind == Markup.ML_REF) { body match { case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => state.add_markup( - command.markup_node( - begin, end, + command.decode_range(range, Command.RefInfo( Position.get_file(props), Position.get_line(props), @@ -110,7 +111,7 @@ } else { state.add_markup( - command.markup_node(begin, end, + command.decode_range(range, Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) } case _ => state @@ -151,21 +152,18 @@ val source: String = span.map(_.source).mkString def source(range: Text.Range): String = source.substring(range.start, range.stop) def length: Int = source.length + val range: Text.Range = Text.Range(0, length) lazy val symbol_index = new Symbol.Index(source) /* markup */ - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = - { - val start = symbol_index.decode(begin - 1) - val stop = symbol_index.decode(end - 1) - new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil) - } + def decode_range(range: Text.Range, info: Any): Markup_Tree.Node = + new Markup_Tree.Node(symbol_index.decode(range), info) /* accumulated results */ - val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source)) + val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty) } diff -r 7766812a01e7 -r e628da370072 src/Pure/PIDE/markup_node.scala --- a/src/Pure/PIDE/markup_node.scala Wed Aug 18 14:04:13 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -/* Title: Pure/PIDE/markup_node.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -Text markup nodes. -*/ - -package isabelle - - -import javax.swing.tree.DefaultMutableTreeNode - - - -case class Markup_Node(val range: Text.Range, val info: Any) - -case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree]) -{ - private def add(branch: Markup_Tree) = // FIXME avoid sort - copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start)) - - private def remove(bs: List[Markup_Tree]) = - copy(branches = branches.filterNot(bs.contains(_))) - - def + (new_tree: Markup_Tree): Markup_Tree = - { - val new_node = new_tree.node - if (node.range contains new_node.range) { - var inserted = false - val new_branches = - branches.map(branch => - if ((branch.node.range contains new_node.range) && !inserted) { - inserted = true - branch + new_tree - } - else branch) - if (!inserted) { - // new_tree did not fit into children of this - // -> insert between this and its branches - val fitting = branches filter(new_node.range contains _.node.range) - (this remove fitting) add ((new_tree /: fitting)(_ + _)) - } - else copy(branches = new_branches) - } - else { - System.err.println("Ignored nonfitting markup: " + new_node) - this - } - } - - def flatten: List[Markup_Node] = - { - var next_x = node.range.start - if (branches.isEmpty) List(this.node) - else { - val filled_gaps = - for { - child <- branches - markups = - if (next_x < child.node.range.start) - new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten - else child.flatten - update = (next_x = child.node.range.stop) - markup <- markups - } yield markup - if (next_x < node.range.stop) - filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info)) - else filled_gaps - } - } -} - - -case class Markup_Text(val markup: List[Markup_Tree], val content: String) -{ - private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup) // FIXME !? - - def + (new_tree: Markup_Tree): Markup_Text = - new Markup_Text((root + new_tree).branches, content) - - def filter(pred: Markup_Node => Boolean): Markup_Text = - { - def filt(tree: Markup_Tree): List[Markup_Tree] = - { - val branches = tree.branches.flatMap(filt(_)) - if (pred(tree.node)) List(tree.copy(branches = branches)) - else branches - } - new Markup_Text(markup.flatMap(filt(_)), content) - } - - def flatten: List[Markup_Node] = markup.flatMap(_.flatten) - - def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode = - { - def swing(tree: Markup_Tree): DefaultMutableTreeNode = - { - val node = swing_node(tree.node) - tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch))) - node - } - swing(root) - } -} diff -r 7766812a01e7 -r e628da370072 src/Pure/PIDE/markup_tree.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/markup_tree.scala Wed Aug 18 23:44:50 2010 +0200 @@ -0,0 +1,113 @@ +/* Title: Pure/PIDE/markup_tree.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Markup trees over nested / non-overlapping text ranges. +*/ + +package isabelle + + +import javax.swing.tree.DefaultMutableTreeNode + +import scala.collection.immutable.SortedMap +import scala.collection.mutable +import scala.annotation.tailrec + + +object Markup_Tree +{ + case class Node(val range: Text.Range, val info: Any) + + + /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */ + + object Branches + { + type Entry = (Node, Markup_Tree) + type T = SortedMap[Node, Entry] + + val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node] + { + def compare(x: Node, y: Node): Int = x.range compare y.range + }) + def update(branches: T, entries: Entry*): T = + branches ++ entries.map(e => (e._1 -> e)) + def make(entries: List[Entry]): T = update(empty, entries:_*) + } + + val empty = new Markup_Tree(Branches.empty) +} + + +case class Markup_Tree(val branches: Markup_Tree.Branches.T) +{ + import Markup_Tree._ + + def + (new_node: Node): Markup_Tree = + { + // FIXME tune overlapping == branches && rest.isEmpty + val (overlapping, rest) = + { + val overlapping = new mutable.ListBuffer[Branches.Entry] + var rest = branches + while (rest.isDefinedAt(new_node)) { + overlapping += rest(new_node) + rest -= new_node + } + (overlapping.toList, rest) + } + overlapping match { + case Nil => + new Markup_Tree(Branches.update(branches, new_node -> empty)) + + case List((node, subtree)) + if node.range != new_node.range && (node.range contains new_node.range) => + new Markup_Tree(Branches.update(branches, node -> (subtree + new_node))) + + case _ if overlapping.forall(e => new_node.range contains e._1.range) => + val new_tree = new Markup_Tree(Branches.make(overlapping)) + new Markup_Tree(Branches.update(rest, new_node -> new_tree)) + + case _ => // FIXME split markup!? + System.err.println("Ignored overlapping markup: " + new_node); this + } + } + + // FIXME depth-first with result markup stack + // FIXME projection to given range + def flatten(parent: Node): List[Node] = + { + val result = new mutable.ListBuffer[Node] + var offset = parent.range.start + for ((_, (node, subtree)) <- branches.iterator) { + if (offset < node.range.start) + result += new Node(Text.Range(offset, node.range.start), parent.info) + result ++= subtree.flatten(node) + offset = node.range.stop + } + if (offset < parent.range.stop) + result += new Node(Text.Range(offset, parent.range.stop), parent.info) + result.toList + } + + def filter(pred: Node => Boolean): Markup_Tree = + { + val bs = branches.toList.flatMap(entry => { + val (_, (node, subtree)) = entry + if (pred(node)) List((node, (node, subtree.filter(pred)))) + else subtree.filter(pred).branches.toList + }) + new Markup_Tree(Branches.empty ++ bs) + } + + def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode) + { + for ((_, (node, subtree)) <- branches) { + val current = swing_node(node) + subtree.swing_tree(current)(swing_node) + parent.add(current) + } + } +} + diff -r 7766812a01e7 -r e628da370072 src/Pure/build-jars --- a/src/Pure/build-jars Wed Aug 18 14:04:13 2010 +0200 +++ b/src/Pure/build-jars Wed Aug 18 23:44:50 2010 +0200 @@ -41,7 +41,7 @@ Isar/token.scala PIDE/command.scala PIDE/document.scala - PIDE/markup_node.scala + PIDE/markup_tree.scala PIDE/text.scala System/cygwin.scala System/download.scala diff -r 7766812a01e7 -r e628da370072 src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Aug 18 14:04:13 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Aug 18 23:44:50 2010 +0200 @@ -279,7 +279,7 @@ for { (command, command_start) <- snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop)) - markup <- snapshot.state(command).highlight.flatten + markup <- snapshot.state(command).highlight val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start) if (abs_stop > start) if (abs_start < stop) diff -r 7766812a01e7 -r e628da370072 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Aug 18 14:04:13 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Aug 18 23:44:50 2010 +0200 @@ -79,7 +79,7 @@ case Some((word, cs)) => val ds = (if (Isabelle_Encoding.is_active(buffer)) - cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _) + cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) else cs).filter(_ != word) if (ds.isEmpty) null else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } @@ -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) { - root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) => + snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) => { val content = command.source(node.range).replace('\n', ' ') val id = command.id @@ -146,7 +146,7 @@ override def getEnd: Position = command_start + node.range.stop override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]" }) - })) + }) } } }