# HG changeset patch
# User wenzelm
# Date 1282555118 -7200
# Node ID 39412530436f0b6a3e07b310aff6d38e3fa01dff
# Parent  9cde57cdd0e379f346d4e37a444fbaedf846edc2# Parent  9f63135f3cbb4db3c4a2c9815de6497c08457baa
merged

diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -143,13 +143,13 @@
 
   private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
     private var next_elem = start
-    def hasNext = next_elem.isDefined
-    def next =
+    def hasNext(): Boolean = next_elem.isDefined
+    def next(): A =
       next_elem match {
         case Some(elem) =>
           next_elem = which.get(elem)
           elem
-        case None => throw new NoSuchElementException("next on empty iterator")
+        case None => Iterator.empty.next()
       }
   }
 
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/General/position.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -22,9 +22,9 @@
 
   def get_range(pos: T): Option[Text.Range] =
     (get_offset(pos), get_end_offset(pos)) match {
-      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
-      case (Some(start), None) => Some(Text.Range(start, start + 1))
-      case (None, _) => None
+      case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
+      case (Some(start), None) => Some(Text.Range(start))
+      case (_, _) => None
     }
 
   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/General/pretty.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -14,12 +14,14 @@
 {
   /* markup trees with physical blocks and breaks */
 
+  def block(body: XML.Body): XML.Tree = Block(2, body)
+
   object Block
   {
-    def apply(i: Int, body: List[XML.Tree]): XML.Tree =
+    def apply(i: Int, body: XML.Body): XML.Tree =
       XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
 
-    def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
+    def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
       tree match {
         case XML.Elem(
           Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
@@ -45,7 +47,7 @@
 
   /* formatted output */
 
-  private def standard_format(tree: XML.Tree): List[XML.Tree] =
+  private def standard_format(tree: XML.Tree): XML.Body =
     tree match {
       case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
       case XML.Text(text) =>
@@ -53,12 +55,12 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  case class Text(tx: List[XML.Tree] = Nil, val pos: Double = 0.0, val nl: Int = 0)
+  case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
     def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
-    def content: List[XML.Tree] = tx.reverse
+    def content: XML.Body = tx.reverse
   }
 
   private val margin_default = 76
@@ -71,8 +73,8 @@
       ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
     }
 
-  def formatted(input: List[XML.Tree], margin: Int = margin_default,
-    metric: String => Double = metric_default): List[XML.Tree] =
+  def formatted(input: XML.Body, margin: Int = margin_default,
+    metric: String => Double = metric_default): XML.Body =
   {
     val breakgain = margin / 20
     val emergencypos = margin / 2
@@ -83,7 +85,7 @@
         case XML.Text(s) => metric(s)
       }
 
-    def breakdist(trees: List[XML.Tree], after: Double): Double =
+    def breakdist(trees: XML.Body, after: Double): Double =
       trees match {
         case Break(_) :: _ => 0.0
         case FBreak :: _ => 0.0
@@ -91,7 +93,7 @@
         case Nil => after
       }
 
-    def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
+    def forcenext(trees: XML.Body): XML.Body =
       trees match {
         case Nil => Nil
         case FBreak :: _ => trees
@@ -99,7 +101,7 @@
         case t :: ts => t :: forcenext(ts)
       }
 
-    def format(trees: List[XML.Tree], blockin: Double, after: Double, text: Text): Text =
+    def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
@@ -129,16 +131,16 @@
     format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
   }
 
-  def string_of(input: List[XML.Tree], margin: Int = margin_default,
+  def string_of(input: XML.Body, margin: Int = margin_default,
       metric: String => Double = metric_default): String =
     formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
 
 
   /* unformatted output */
 
-  def unformatted(input: List[XML.Tree]): List[XML.Tree] =
+  def unformatted(input: XML.Body): XML.Body =
   {
-    def fmt(tree: XML.Tree): List[XML.Tree] =
+    def fmt(tree: XML.Tree): XML.Body =
       tree match {
         case Block(_, body) => body.flatMap(fmt)
         case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
@@ -149,6 +151,6 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: List[XML.Tree]): String =
+  def str_of(input: XML.Body): String =
     unformatted(input).iterator.flatMap(XML.content).mkString
 }
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/Isar/toplevel.scala
--- a/src/Pure/Isar/toplevel.scala	Sun Aug 22 14:27:30 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/*  Title:      Pure/Isar/toplevel.scala
-    Author:     Makarius
-
-Isabelle/Isar toplevel transactions.
-*/
-
-package isabelle
-
-
-object Toplevel
-{
-  sealed abstract class Status
-  case class Forked(forks: Int) extends Status
-  case object Unprocessed extends Status
-  case object Finished extends Status
-  case object Failed extends Status
-
-  def command_status(markup: XML.Body): Status =
-  {
-    val forks = (0 /: markup) {
-      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
-      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
-      case (i, _) => i
-    }
-    if (forks != 0) Forked(forks)
-    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
-      Failed
-    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
-      Finished
-    else Unprocessed
-  }
-}
-
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -14,20 +14,11 @@
 
 object Command
 {
-  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
-    override def toString = kind
-  }
-  case class TypeInfo(ty: String)
-  case class RefInfo(file: Option[String], line: Option[Int],
-    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
-
-
-
   /** accumulated results from prover **/
 
   case class State(
     val command: Command,
-    val status: List[XML.Tree],
+    val status: List[Markup],
     val reverse_results: List[XML.Tree],
     val markup: Markup_Tree)
   {
@@ -37,86 +28,31 @@
 
     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 markup_root_node: Markup_Tree.Node =
-      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] =
-    {
-      markup.filter(_.info match {
-        case Command.HighlightInfo(_, _) => true
-        case _ => false
-      }).flatten(markup_root_node)
-    }
+    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
 
-    private lazy val types: List[Markup_Tree.Node] =
-      markup.filter(_.info match {
-        case Command.TypeInfo(_) => true
-        case _ => false }).flatten(markup_root_node)
-
-    def type_at(pos: Text.Offset): Option[String] =
-    {
-      types.find(_.range.contains(pos)) match {
-        case Some(t) =>
-          t.info match {
-            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
-            case _ => None
-          }
-        case None => None
-      }
-    }
-
-    private lazy val refs: List[Markup_Tree.Node] =
-      markup.filter(_.info match {
-        case Command.RefInfo(_, _, _, _) => true
-        case _ => false }).flatten(markup_root_node)
-
-    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
-      refs.find(_.range.contains(pos))
+    def markup_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
 
 
     /* message dispatch */
 
     def accumulate(message: XML.Tree): Command.State =
       message match {
-        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
+        case XML.Elem(Markup(Markup.STATUS, _), body) =>  // FIXME explicit checks!?
+          copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
 
-        case XML.Elem(Markup(Markup.REPORT, _), elems) =>
-          (this /: elems)((state, elem) =>
-            elem match {
-              case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
-                atts match {
-                  case Position.Range(range) =>
-                    if (kind == Markup.ML_TYPING) {
-                      val info = Pretty.string_of(body, margin = 40)
-                      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.decode_range(range,
-                              Command.RefInfo(
-                                Position.get_file(props),
-                                Position.get_line(props),
-                                Position.get_id(props),
-                                Position.get_offset(props))))
-                        case _ => state
-                      }
-                    }
-                    else {
-                      state.add_markup(
-                        command.decode_range(range,
-                          Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
-                    }
-                  case _ => state
-                }
-              case _ => System.err.println("Ignored report message: " + elem); state
+        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+          (this /: msgs)((state, msg) =>
+            msg match {
+              case XML.Elem(Markup(name, atts), args)
+              if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
+                val range = command.decode(Position.get_range(atts).get)
+                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
+                add_markup(info)
+              case _ => System.err.println("Ignored report message: " + msg); state
             })
         case _ => add_result(message)
       }
@@ -152,15 +88,12 @@
   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 decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
-    new Markup_Tree.Node(symbol_index.decode(range), info)
+  def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
+  def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
 
 
   /* accumulated results */
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -65,11 +65,11 @@
     def command_start(cmd: Command): Option[Text.Offset] =
       command_starts.find(_._1 == cmd).map(_._2)
 
-    def command_range(i: Text.Offset): Iterator[(Command, Text.Offset)] =
+    def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
       command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
 
-    def command_range(i: Text.Offset, j: Text.Offset): Iterator[(Command, Text.Offset)] =
-      command_range(i) takeWhile { case (_, start) => start < j }
+    def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
+      command_range(range.start) takeWhile { case (_, start) => start < range.stop }
 
     def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
     {
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Mon Aug 23 11:18:38 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/PIDE/isar_document.ML
     Author:     Makarius
 
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
 *)
 
 structure Isar_Document: sig end =
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/PIDE/isar_document.scala
     Author:     Makarius
 
-Protocol commands for interactive Isar documents.
+Protocol message formats for interactive Isar documents.
 */
 
 package isabelle
@@ -9,7 +9,7 @@
 
 object Isar_Document
 {
-  /* protocol messages */
+  /* document editing */
 
   object Assign {
     def unapply(msg: XML.Tree)
@@ -32,6 +32,28 @@
         case _ => None
       }
   }
+
+
+  /* toplevel transactions */
+
+  sealed abstract class Status
+  case class Forked(forks: Int) extends Status
+  case object Unprocessed extends Status
+  case object Finished extends Status
+  case object Failed extends Status
+
+  def command_status(markup: List[Markup]): Status =
+  {
+    val forks = (0 /: markup) {
+      case (i, Markup(Markup.FORKED, _)) => i + 1
+      case (i, Markup(Markup.JOINED, _)) => i - 1
+      case (i, _) => i
+    }
+    if (forks != 0) Forked(forks)
+    else if (markup.exists(_.name == Markup.FAILED)) Failed
+    else if (markup.exists(_.name == Markup.FINISHED)) Finished
+    else Unprocessed
+  }
 }
 
 
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -17,26 +17,30 @@
 
 object Markup_Tree
 {
-  case class Node(val range: Text.Range, val info: Any)
-  {
-    def contains(that: Node): Boolean = this.range contains that.range
-    def intersect(r: Text.Range): Node = Node(range.intersect(r), info)
-  }
-
-
-  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
+  /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
 
   object Branches
   {
-    type Entry = (Node, Markup_Tree)
-    type T = SortedMap[Node, Entry]
+    type Entry = (Text.Info[Any], Markup_Tree)
+    type T = SortedMap[Text.Range, Entry]
 
-    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
+    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
       {
-        def compare(x: Node, y: Node): Int = x.range compare y.range
+        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
       })
-    def update(branches: T, entries: Entry*): T =
-      branches ++ entries.map(e => (e._1 -> e))
+
+    def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
+
+    def overlapping(range: Text.Range, branches: T): T =
+    {
+      val start = Text.Range(range.start)
+      val stop = Text.Range(range.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)
+      }
+    }
   }
 
   val empty = new Markup_Tree(Branches.empty)
@@ -47,95 +51,77 @@
 {
   import Markup_Tree._
 
-  def + (new_node: Node): Markup_Tree =
+  override def toString =
+    branches.toList.map(_._2) match {
+      case Nil => "Empty"
+      case list => list.mkString("Tree(", ",", ")")
+    }
+
+  def + (new_info: Text.Info[Any]): Markup_Tree =
   {
-    branches.get(new_node) match {
+    val new_range = new_info.range
+    branches.get(new_range) match {
       case None =>
-        new Markup_Tree(Branches.update(branches, new_node -> empty))
-      case Some((node, subtree)) =>
-        if (node.range != new_node.range && node.contains(new_node))
-          new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
-        else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
-          new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
+        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))
+          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)))
         else {
-          var overlapping = Branches.empty
-          var rest = branches
-          while (rest.isDefinedAt(new_node)) {
-            overlapping = Branches.update(overlapping, rest(new_node))
-            rest -= new_node
+          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)
+            new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
           }
-          if (overlapping.forall(e => new_node.contains(e._1)))
-            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
           else { // FIXME split markup!?
-            System.err.println("Ignored overlapping markup: " + new_node)
+            System.err.println("Ignored overlapping markup information: " + new_info)
             this
           }
         }
     }
   }
 
-  // FIXME depth-first with result markup stack
-  // FIXME projection to given range
-  def flatten(parent: Node): List[Node] =
+  def select[A](root_range: Text.Range)
+    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
   {
-    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
+    def stream(parent: Text.Info[A], bs: Branches.T): 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
+
+      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 (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)
+    stream(Text.Info(root_range, default), branches)
   }
 
-  def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
+  def swing_tree(parent: DefaultMutableTreeNode)
+    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
   {
-    def stream(parent: Node, bs: Branches.T): Stream[Node] =
-    {
-      val start = Node(parent.range.start_range, Nil)
-      val stop = Node(parent.range.stop_range, Nil)
-      val substream =
-        (for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield {
-          if (sel.isDefinedAt(node))
-            stream(node.intersect(parent.range), subtree.branches)
-          else stream(parent, subtree.branches)
-        }).flatten
-
-      def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
-        s match {
-          case node #:: rest =>
-            if (last < node.range.start)
-              parent.intersect(Text.Range(last, node.range.start)) #::
-                node #:: padding(node.range.stop, rest)
-            else node #:: padding(node.range.stop, rest)
-          case Stream.Empty =>  // FIXME
-            if (last < parent.range.stop)
-            Stream(parent.intersect(Text.Range(last, parent.range.stop)))
-            else Stream.Empty
-        }
-      padding(parent.range.start, substream)
-    }
-    // FIXME handle disjoint range!?
-    stream(Node(range, Nil), branches)
-  }
-
-  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
-  {
-    for ((_, (node, subtree)) <- branches) {
-      val current = swing_node(node)
+    for ((_, (info, subtree)) <- branches) {
+      val current = swing_node(info)
       subtree.swing_tree(current)(swing_node)
       parent.add(current)
     }
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -15,37 +15,38 @@
   type Offset = Int
 
 
-  /* range: interval with total quasi-ordering */
+  /* range -- with total quasi-ordering */
 
   object Range
   {
-    object Ordering extends scala.math.Ordering[Range]
-    {
-      override def compare(r1: Range, r2: Range): Int = r1 compare r2
-    }
+    def apply(start: Offset): Range = Range(start, start)
   }
 
   sealed case class Range(val start: Offset, val stop: Offset)
   {
+    // denotation: {start} Un {i. start < i & i < stop}
     require(start <= stop)
 
+    override def toString = "[" + start.toString + ":" + stop.toString + "]"
+
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = map(_ + i)
-    def contains(i: Offset): Boolean = start <= i && i < stop
-    def contains(that: Range): Boolean =
-      this == that || this.contains(that.start) && that.stop <= this.stop
-    def overlaps(that: Range): Boolean =
-      this == that || this.contains(that.start) || that.contains(this.start)
-    def compare(that: Range): Int =
-      if (overlaps(that)) 0
-      else if (this.start < that.start) -1
-      else 1
+    def -(i: Offset): Range = map(_ - i)
+    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)
+    def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
 
-    def start_range: Range = Range(start, start)
-    def stop_range: Range = Range(stop, stop)
+    def restrict(that: Range): Range =
+      Range(this.start max that.start, this.stop min that.stop)
+  }
+
 
-    def intersect(that: Range): Range =
-      Range(this.start max that.start, this.stop min that.stop)
+  /* information associated with text range */
+
+  case class Info[A](val range: Text.Range, val info: A)
+  {
+    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
   }
 
 
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -95,7 +95,7 @@
 
   private val xml_cache = new XML.Cache(131071)
 
-  private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
+  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {
     if (pid.isEmpty && kind == Markup.INIT)
       pid = props.find(_._1 == Markup.PID).map(_._1)
@@ -257,7 +257,7 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(): List[XML.Tree] =
+      def read_chunk(): XML.Body =
       {
         //{{{
         // chunk size
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -60,7 +60,7 @@
   /** main actor **/
 
   @volatile private var syntax = new Outer_Syntax(system.symbols)
-  def current_syntax: Outer_Syntax = syntax
+  def current_syntax(): Outer_Syntax = syntax
 
   @volatile private var global_state = Document.State.init
   private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/Thy/html.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -41,7 +41,7 @@
 
   // document markup
 
-  def span(cls: String, body: List[XML.Tree]): XML.Elem =
+  def span(cls: String, body: XML.Body): XML.Elem =
     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
 
   def hidden(txt: String): XML.Elem =
@@ -50,9 +50,9 @@
   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
 
-  def spans(input: XML.Tree, original_data: Boolean = false): List[XML.Tree] =
+  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
   {
-    def html_spans(tree: XML.Tree): List[XML.Tree] =
+    def html_spans(tree: XML.Tree): XML.Body =
       tree match {
         case XML.Elem(Markup(name, _), ts) =>
           if (original_data)
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -84,7 +84,7 @@
             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
 
           val sources = range.flatMap(_.span.map(_.source))
-          val spans0 = parse_spans(session.current_syntax.scan(sources.mkString))
+          val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
 
           val (before_edit, spans1) =
             if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/build-jars	Mon Aug 23 11:18:38 2010 +0200
@@ -37,7 +37,6 @@
   Isar/keyword.scala
   Isar/outer_syntax.scala
   Isar/parse.scala
-  Isar/toplevel.scala
   Isar/token.scala
   PIDE/command.scala
   PIDE/document.scala
diff -r 9cde57cdd0e3 -r 39412530436f src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/library.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -79,7 +79,7 @@
     def next(): CharSequence =
       state match {
         case Some((s, i)) => { state = next_chunk(i); s }
-        case None => throw new NoSuchElementException("next on empty iterator")
+        case None => Iterator.empty.next()
       }
   }
 
diff -r 9cde57cdd0e3 -r 39412530436f src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -257,14 +257,17 @@
     override def markTokens(prev: TokenMarker.LineContext,
         handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
     {
+      // FIXME proper synchronization / thread context (!??)
+      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+
       val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
       val line = if (prev == null) 0 else previous.line + 1
       val context = new Document_Model.Token_Markup.LineContext(line, previous)
+
       val start = buffer.getLineStartOffset(line)
       val stop = start + line_segment.count
-
-      // FIXME proper synchronization / thread context (!??)
-      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+      val range = Text.Range(start, stop)
+      val former_range = snapshot.revert(range)
 
       /* FIXME
       for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -275,35 +278,38 @@
       def handle_token(style: Byte, offset: Text.Offset, length: Int) =
         handler.handleToken(line_segment, style, offset, length, context)
 
+      val syntax = session.current_syntax()
+      val token_markup: PartialFunction[Text.Info[Any], Byte] =
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
+        if syntax.keyword_kind(name).isDefined =>
+          Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
+
+        case Text.Info(_, XML.Elem(Markup(name, _), _))
+        if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
+          Document_Model.Token_Markup.token_style(name)
+      }
+
       var next_x = start
       for {
-        (command, command_start) <-
-          snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
-        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)
+        (command, command_start) <- snapshot.node.command_range(former_range)
+        info <- snapshot.state(command).markup.
+          select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
+        val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
+        if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
+      }
+      {
         val token_start = (abs_start - start) max 0
         val token_length =
           (abs_stop - abs_start) -
           ((start - abs_start) max 0) -
           ((abs_stop - stop) max 0)
-      }
-      {
-        val token_type =
-          markup.info match {
-            case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
-              Document_Model.Token_Markup.command_style(kind)
-            case Command.HighlightInfo(kind, _) =>
-              Document_Model.Token_Markup.token_style(kind)
-            case _ => Token.NULL
-          }
-        if (start + token_start > next_x)
+        if (start + token_start > next_x)  // FIXME ??
           handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
-        handle_token(token_type, token_start, token_length)
+        handle_token(info.info, token_start, token_length)
         next_x = start + token_start + token_length
       }
-      if (next_x < stop)
+      if (next_x < stop)  // FIXME ??
         handle_token(Token.COMMENT1, next_x - start, stop - next_x)
 
       handle_token(Token.END, line_segment.count, 0)
diff -r 9cde57cdd0e3 -r 39412530436f src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -29,11 +29,11 @@
     val state = snapshot.state(command)
     if (snapshot.is_outdated) new Color(240, 240, 240)
     else
-      Toplevel.command_status(state.status) match {
-        case Toplevel.Forked(i) if i > 0 => new Color(255, 228, 225)
-        case Toplevel.Finished => new Color(234, 248, 255)
-        case Toplevel.Failed => new Color(255, 193, 193)
-        case Toplevel.Unprocessed => new Color(255, 228, 225)
+      Isar_Document.command_status(state.status) match {
+        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
+        case Isar_Document.Finished => new Color(234, 248, 255)
+        case Isar_Document.Failed => new Color(255, 193, 193)
+        case Isar_Document.Unprocessed => new Color(255, 228, 225)
         case _ => Color.red
       }
   }
@@ -202,10 +202,12 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          snapshot.state(command).type_at(offset - command_start) match {
-            case Some(text) => Isabelle.tooltip(text)
-            case None => null
-          }
+          (snapshot.state(command).markup.select(Text.Range(offset) - command_start) {
+            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+              val typing =
+                Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
+              Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
+          } { null }).head.info
         case None => null
       }
     }
diff -r 9cde57cdd0e3 -r 39412530436f src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -116,7 +116,7 @@
   /* internal messages */
 
   private case class Resize(font_family: String, font_size: Int)
-  private case class Render(body: List[XML.Tree])
+  private case class Render(body: XML.Body)
   private case object Refresh
 
   private val main_actor = actor {
@@ -127,7 +127,7 @@
     var current_font_family = ""
     var current_font_size: Int = 0
     var current_margin: Int = 0
-    var current_body: List[XML.Tree] = Nil
+    var current_body: XML.Body = Nil
 
     def resize(font_family: String, font_size: Int)
     {
@@ -152,7 +152,7 @@
 
     def refresh() { render(current_body) }
 
-    def render(body: List[XML.Tree])
+    def render(body: XML.Body)
     {
       current_body = body
       val html_body =
@@ -190,5 +190,5 @@
 
   def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   def refresh() { main_actor ! Refresh }
-  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+  def render(body: XML.Body) { main_actor ! Render(body) }
 }
diff -r 9cde57cdd0e3 -r 39412530436f src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -38,37 +38,41 @@
 
 class Isabelle_Hyperlinks extends HyperlinkSource
 {
-  def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
+  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
   {
     Swing_Thread.assert()
     Document_Model(buffer) match {
       case Some(model) =>
         val snapshot = model.snapshot()
-        val offset = snapshot.revert(original_offset)
+        val offset = snapshot.revert(buffer_offset)
         snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
-            snapshot.state(command).ref_at(offset - command_start) match {
-              case Some(ref) =>
-                val Text.Range(begin, end) = snapshot.convert(ref.range + command_start)
+            (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), _)))) =>
+                val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
                 val line = buffer.getLineOfOffset(begin)
-                ref.info match {
-                  case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
+
+                (Position.get_file(props), Position.get_line(props)) match {
+                  case (Some(ref_file), Some(ref_line)) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)
-                  case Command.RefInfo(_, _, Some(id), Some(offset)) =>
-                    snapshot.lookup_command(id) match {  // FIXME Command_ID vs. Exec_ID (!??)
-                      case Some(ref_cmd) =>
-                        snapshot.node.command_start(ref_cmd) match {
-                          case Some(ref_cmd_start) =>
-                            new Internal_Hyperlink(begin, end, line,
-                              snapshot.convert(ref_cmd_start + offset - 1))
-                          case None => null // FIXME external ref
+                  case _ =>
+                    (Position.get_id(props), Position.get_offset(props)) match {
+                      case (Some(ref_id), Some(ref_offset)) =>
+                        snapshot.lookup_command(ref_id) match {
+                          case Some(ref_cmd) =>
+                            snapshot.node.command_start(ref_cmd) match {
+                              case Some(ref_cmd_start) =>
+                                new Internal_Hyperlink(begin, end, line,
+                                  snapshot.convert(ref_cmd_start + ref_cmd.decode(ref_offset)))
+                              case None => null
+                            }
+                          case None => null
                         }
                       case _ => null
                     }
-                  case _ => null
                 }
-              case None => null
-            }
+            } { null }).head.info
           case None => null
         }
       case None => null
diff -r 9cde57cdd0e3 -r 39412530436f src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Aug 23 11:18:38 2010 +0200
@@ -72,7 +72,7 @@
     val start = buffer.getLineStartOffset(line)
     val text = buffer.getSegment(start, caret - start)
 
-    val completion = Isabelle.session.current_syntax.completion
+    val completion = Isabelle.session.current_syntax().completion
 
     completion.complete(text) match {
       case None => null
@@ -97,7 +97,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)
+      (command, command_start) <- snapshot.node.command_range()
       if command.is_command && !stopped
     }
     {
@@ -128,22 +128,22 @@
 
     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) =>
+    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+      snapshot.state(command).markup_root.swing_tree(root)((info: Text.Info[Any]) =>
           {
-            val content = command.source(node.range).replace('\n', ' ')
+            val content = command.source(info.range).replace('\n', ' ')
             val id = command.id
 
             new DefaultMutableTreeNode(new IAsset {
               override def getIcon: Icon = null
               override def getShortString: String = content
-              override def getLongString: String = node.info.toString
+              override def getLongString: String = info.info.toString
               override def getName: String = Markup.Long(id)
               override def setName(name: String) = ()
               override def setStart(start: Position) = ()
-              override def getStart: Position = command_start + node.range.start
+              override def getStart: Position = command_start + info.range.start
               override def setEnd(end: Position) = ()
-              override def getEnd: Position = command_start + node.range.stop
+              override def getEnd: Position = command_start + info.range.stop
               override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
             })
           })