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;
--- 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) }
}
--- 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(_))
}
--- 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)
}
--- 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)
- }
-}
--- /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)
+ }
+ }
+}
+
--- 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
--- 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)
--- 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 + "]"
})
- }))
+ })
}
}
}