# HG changeset patch # User wenzelm # Date 1282727638 -7200 # Node ID fb30a006384a604c0b84dadcd234fcfde714eefe # Parent 0e2596019119dc57db7e58c43f5b03c597c3aee7# Parent fcd56e6a04b968dbade529b815a96f1a5a6dcd24 merged diff -r 0e2596019119 -r fb30a006384a src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Aug 25 09:44:54 2010 +0200 +++ b/src/Pure/PIDE/command.scala Wed Aug 25 11:13:58 2010 +0200 @@ -26,10 +26,10 @@ def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info) - def markup_root_info: Text.Info[Any] = + def root_info: Text.Info[Any] = new Text.Info(command.range, - XML.Elem(Markup(Markup.STATUS, Nil), status.map(XML.Elem(_, Nil)))) - def markup_root: Markup_Tree = markup + markup_root_info + XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil)))) + def root_markup: Markup_Tree = markup + root_info /* message dispatch */ diff -r 0e2596019119 -r fb30a006384a src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Wed Aug 25 09:44:54 2010 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Wed Aug 25 11:13:58 2010 +0200 @@ -11,8 +11,6 @@ import javax.swing.tree.DefaultMutableTreeNode import scala.collection.immutable.SortedMap -import scala.collection.mutable -import scala.annotation.tailrec object Markup_Tree @@ -30,15 +28,16 @@ }) def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry) + def single(entry: Entry): T = update(empty, entry) - def overlapping(range: Text.Range, branches: T): T = + def overlapping(range: Text.Range, branches: T): T = // FIXME special cases!? { val start = Text.Range(range.start) val stop = Text.Range(range.stop) + val bs = branches.range(start, stop) branches.get(stop) match { - case Some(end) if range overlaps end._1.range => - update(branches.range(start, stop), end) - case _ => branches.range(start, stop) + case Some(end) if range overlaps end._1.range => update(bs, end) + case _ => bs } } } @@ -65,15 +64,18 @@ new Markup_Tree(Branches.update(branches, new_info -> empty)) case Some((info, subtree)) => val range = info.range - if (range != new_range && range.contains(new_range)) + if (range.contains(new_range)) new Markup_Tree(Branches.update(branches, info -> (subtree + new_info))) else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1)) - new Markup_Tree(Branches.update(Branches.empty, (new_info -> this))) + new Markup_Tree(Branches.single(new_info -> this)) else { val body = Branches.overlapping(new_range, branches) if (body.forall(e => new_range.contains(e._1))) { - val rest = (Branches.empty /: branches)((rest, entry) => - if (body.isDefinedAt(entry._1)) rest else rest + entry) + val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 + if (body.size > 1) + (Branches.empty /: branches)((rest, entry) => + if (body.isDefinedAt(entry._1)) rest else rest + entry) + else branches new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body))) } else { // FIXME split markup!? @@ -84,37 +86,39 @@ } } + private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] = + Branches.overlapping(range, branches).toStream + def select[A](root_range: Text.Range) (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] = { - def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] = + def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]) + : Stream[Text.Info[A]] = { - val range = parent.range - val substream = - (for ((info_range, (info, subtree)) <- Branches.overlapping(range, bs).toStream) yield { - if (result.isDefinedAt(info)) { - val current = Text.Info(info_range.restrict(range), result(info)) - stream(current, subtree.branches) - } - else stream(parent.restrict(info_range), subtree.branches) - }).flatten + stack match { + case (parent, (range, (info, tree)) #:: more) :: rest => + val subrange = range.restrict(root_range) + val subtree = tree.overlapping(subrange) + val start = subrange.start - def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] = - s match { - case info #:: rest => - val Text.Range(start, stop) = info.range - if (last < start) - parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest) - else info #:: padding(stop, rest) - case Stream.Empty => - if (last < range.stop) - Stream(parent.restrict(Text.Range(last, range.stop))) - else Stream.Empty - } - if (substream.isEmpty) Stream(parent) - else padding(range.start, substream) + if (result.isDefinedAt(info)) { + val next = Text.Info(subrange, result(info)) + val nexts = stream(start, (next, subtree) :: (parent, more) :: rest) + if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts + else nexts + } + else stream(last, (parent, subtree #::: more) :: rest) + + case (parent, Stream.Empty) :: rest => + val stop = parent.range.stop + val nexts = stream(stop, rest) + if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts + else nexts + + case Nil => Stream(Text.Info(Text.Range(last, root_range.stop), default)) + } } - stream(Text.Info(root_range, default), branches) + stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range)))) } def swing_tree(parent: DefaultMutableTreeNode) diff -r 0e2596019119 -r fb30a006384a src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Wed Aug 25 09:44:54 2010 +0200 +++ b/src/Pure/PIDE/text.scala Wed Aug 25 11:13:58 2010 +0200 @@ -32,6 +32,9 @@ def map(f: Offset => Offset): Range = Range(f(start), f(stop)) def +(i: Offset): Range = map(_ + i) def -(i: Offset): Range = map(_ - i) + + def is_singleton: Boolean = start == stop + def contains(i: Offset): Boolean = start == i || start < i && i < stop def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start) diff -r 0e2596019119 -r fb30a006384a src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Aug 25 09:44:54 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Aug 25 11:13:58 2010 +0200 @@ -198,6 +198,7 @@ val offset = snapshot.revert(text_area.xyToOffset(x, y)) snapshot.node.command_at(offset) match { case Some((command, command_start)) => + // FIXME Isar_Document.Tooltip extractor (snapshot.state(command).markup.select(Text.Range(offset) - command_start) { case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => val typing = diff -r 0e2596019119 -r fb30a006384a src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Aug 25 09:44:54 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Aug 25 11:13:58 2010 +0200 @@ -48,6 +48,7 @@ val offset = snapshot.revert(buffer_offset) snapshot.node.command_at(offset) match { case Some((command, command_start)) => + // FIXME Isar_Document.Hyperlink extractor (snapshot.state(command).markup.select(Text.Range(offset) - command_start) { case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => diff -r 0e2596019119 -r fb30a006384a src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Aug 25 09:44:54 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Aug 25 11:13:58 2010 +0200 @@ -130,22 +130,28 @@ val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range() if !stopped) { - snapshot.state(command).markup_root.swing_tree(root)((info: Text.Info[Any]) => + snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) => { + val range = info.range + command_start val content = command.source(info.range).replace('\n', ' ') - val id = command.id + val info_text = + info.info match { + case elem @ XML.Elem(_, _) => + Pretty.formatted(List(elem), margin = 40).mkString("\n") + case x => x.toString + } new DefaultMutableTreeNode(new IAsset { override def getIcon: Icon = null override def getShortString: String = content - override def getLongString: String = info.info.toString - override def getName: String = Markup.Long(id) + override def getLongString: String = info_text + override def getName: String = command.toString override def setName(name: String) = () override def setStart(start: Position) = () - override def getStart: Position = command_start + info.range.start + override def getStart: Position = range.start override def setEnd(end: Position) = () - override def getEnd: Position = command_start + info.range.stop - override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]" + override def getEnd: Position = range.stop + override def toString = "\"" + content + "\" " + range.toString }) }) }