--- a/src/Pure/PIDE/command.scala Wed Aug 25 11:10:08 2010 +0200
+++ b/src/Pure/PIDE/command.scala Wed Aug 25 11:30:45 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 */
--- a/src/Pure/PIDE/markup_tree.scala Wed Aug 25 11:10:08 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Wed Aug 25 11:30:45 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)
--- a/src/Pure/PIDE/text.scala Wed Aug 25 11:10:08 2010 +0200
+++ b/src/Pure/PIDE/text.scala Wed Aug 25 11:30:45 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)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Aug 25 11:10:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Aug 25 11:30:45 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 =
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Aug 25 11:10:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Aug 25 11:30:45 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), _)))) =>
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Aug 25 11:10:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Aug 25 11:30:45 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
})
})
}