renamed Markup_Tree.Node to Text.Info;
Markup_Tree.select: body may depend on full Text.Info, including range;
tuned;

--- a/src/Pure/PIDE/command.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -28,11 +28,11 @@
 
     def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
 
-    def add_markup(node: Markup_Tree.Node[Any]): State = copy(markup = markup + node)
+    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
 
-    def markup_root_node: Markup_Tree.Node[Any] =
-      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
-    def markup_root: Markup_Tree = markup + markup_root_node
+    def markup_root_info: Text.Info[Any] =
+      new Text.Info(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
+    def markup_root: Markup_Tree = markup + markup_root_info
 
 
     /* message dispatch */
@@ -47,8 +47,8 @@
               if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
                 val range = command.decode_range(Position.get_range(atts).get)
                 val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
-                val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args))
-                add_markup(node)
+                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)

--- a/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -17,31 +17,24 @@
 
 object Markup_Tree
 {
-  case class Node[A](val range: Text.Range, val info: A)
-  {
-    def contains[B](that: Node[B]): Boolean = this.range contains that.range
-    def restrict(r: Text.Range): Node[A] = Node(range.restrict(r), info)
-  }
-
-
   /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
 
   object Branches
   {
-    type Entry = (Node[Any], Markup_Tree)
-    type T = SortedMap[Node[Any], Entry]
+    type Entry = (Text.Info[Any], Markup_Tree)
+    type T = SortedMap[Text.Info[Any], Entry]
 
-    val empty = SortedMap.empty[Node[Any], Entry](new scala.math.Ordering[Node[Any]]
+    val empty = SortedMap.empty[Text.Info[Any], Entry](new scala.math.Ordering[Text.Info[Any]]
       {
-        def compare(x: Node[Any], y: Node[Any]): Int = x.range compare y.range
+        def compare(x: Text.Info[Any], y: Text.Info[Any]): Int = x.range compare y.range
       })
 
     def update(branches: T, entry: Entry): T = branches + (entry._1 -> entry)
 
     def overlapping(range: Text.Range, branches: T): T =
     {
-      val start = Node[Any](Text.Range(range.start), Nil)
-      val stop = Node[Any](Text.Range(range.stop), Nil)
+      val start = Text.Info[Any](Text.Range(range.start), Nil)
+      val stop = Text.Info[Any](Text.Range(range.stop), Nil)
       branches.get(stop) match {
         case Some(end) if range overlaps end._1.range =>
           update(branches.range(start, stop), end)
@@ -64,49 +57,50 @@
       case list => list.mkString("Tree(", ",", ")")
     }
 
-  def + (new_node: Node[Any]): Markup_Tree =
+  def + (new_info: Text.Info[Any]): Markup_Tree =
   {
-    branches.get(new_node) match {
+    branches.get(new_info) 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)) =>
+        if (info.range != new_info.range && info.contains(new_info))
+          new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
+        else if (new_info.contains(branches.head._1) && new_info.contains(branches.last._1))
+          new Markup_Tree(Branches.update(Branches.empty, (new_info -> this)))
         else {
-          val body = Branches.overlapping(new_node.range, branches)
-          if (body.forall(e => new_node.contains(e._1))) {
+          val body = Branches.overlapping(new_info.range, branches)
+          if (body.forall(e => new_info.contains(e._1))) {
             val rest = (branches /: body) { case (bs, (e, _)) => bs - e }
-            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(body)))
+            new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
           }
           else { // FIXME split markup!?
-            System.err.println("Ignored overlapping markup: " + new_node)
+            System.err.println("Ignored overlapping markup information: " + new_info)
             this
           }
         }
     }
   }
 
-  def select[A](root: Node[A])(sel: PartialFunction[Any, A]): Stream[Node[A]] =
+  def select[A](root: Text.Info[A])(sel: PartialFunction[Text.Info[Any], A]): Stream[Text.Info[A]] =
   {
-    def stream(parent: Node[A], bs: Branches.T): Stream[Node[A]] =
+    def stream(parent: Text.Info[A], bs: Branches.T): Stream[Text.Info[A]] =
     {
       val substream =
-        (for ((_, (node, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
-          if (sel.isDefinedAt(node.info)) {
-            val current = Node(node.range.restrict(parent.range), sel(node.info))
+        (for ((_, (info, subtree)) <- Branches.overlapping(parent.range, bs).toStream) yield {
+          if (sel.isDefinedAt(info)) {
+            val current = Text.Info(info.range.restrict(parent.range), sel(info))
             stream(current, subtree.branches)
           }
-          else stream(parent.restrict(node.range), subtree.branches)
+          else stream(parent.restrict(info.range), subtree.branches)
         }).flatten
 
-      def padding(last: Text.Offset, s: Stream[Node[A]]): Stream[Node[A]] =
+      def padding(last: Text.Offset, s: Stream[Text.Info[A]]): Stream[Text.Info[A]] =
         s match {
-          case (node @ Node(Text.Range(start, stop), _)) #:: rest =>
+          case info #:: rest =>
+            val Text.Range(start, stop) = info.range
             if (last < start)
-              parent.restrict(Text.Range(last, start)) #:: node #:: padding(stop, rest)
-            else node #:: padding(stop, rest)
+              parent.restrict(Text.Range(last, start)) #:: info #:: padding(stop, rest)
+            else info #:: padding(stop, rest)
           case Stream.Empty =>
             if (last < parent.range.stop)
               Stream(parent.restrict(Text.Range(last, parent.range.stop)))
@@ -118,10 +112,11 @@
     stream(root, branches)
   }
 
-  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node[Any] => DefaultMutableTreeNode)
+  def swing_tree(parent: DefaultMutableTreeNode)
+    (swing_node: Text.Info[Any] => 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)
     }

--- a/src/Pure/PIDE/text.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -42,6 +42,15 @@
   }
 
 
+  /* information associated with text range */
+
+  case class Info[A](val range: Text.Range, val info: A)
+  {
+    def contains[B](that: Info[B]): Boolean = this.range contains that.range
+    def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
+  }
+
+
   /* editing */
 
   object Edit

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -279,13 +279,13 @@
         handler.handleToken(line_segment, style, offset, length, context)
 
       val syntax = session.current_syntax()
-      val token_markup: PartialFunction[Any, Byte] =
+      val token_markup: PartialFunction[Text.Info[Any], Byte] =
       {
-        case XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)
+        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 XML.Elem(Markup(name, _), _)
+        case Text.Info(_, XML.Elem(Markup(name, _), _))
         if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
           Document_Model.Token_Markup.token_style(name)
       }
@@ -293,10 +293,9 @@
       var next_x = start
       for {
         (command, command_start) <- snapshot.node.command_range(former_range)
-        val root_node =
-          Markup_Tree.Node((former_range - command_start).restrict(command.range), Token.NULL)
-        node <- snapshot.state(command).markup.select(root_node)(token_markup)
-        val Text.Range(abs_start, abs_stop) = snapshot.convert(node.range + command_start)
+        val root = Text.Info((former_range - command_start).restrict(command.range), Token.NULL)
+        info <- snapshot.state(command).markup.select(root)(token_markup)
+        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!?)
       }
       {
@@ -307,7 +306,7 @@
           ((abs_stop - stop) max 0)
         if (start + token_start > next_x)  // FIXME ??
           handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
-        handle_token(node.info, token_start, token_length)
+        handle_token(info.info, token_start, token_length)
         next_x = start + token_start + token_length
       }
       if (next_x < stop)  // FIXME ??

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -202,13 +202,12 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          val root_node =
-            Markup_Tree.Node[Option[XML.Body]]((Text.Range(offset) - command_start), None)
-          snapshot.state(command).markup.select(root_node) {
-            case XML.Elem(Markup(Markup.ML_TYPING, _), body) => Some(body)
+          val root = Text.Info[Option[XML.Body]]((Text.Range(offset) - command_start), None)
+          snapshot.state(command).markup.select(root) {
+            case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => Some(body)
           } match {
             // FIXME use original node range, not restricted version
-            case Markup_Tree.Node(range, Some(body)) #:: _ =>
+            case Text.Info(range, Some(body)) #:: _ =>
               val typing =
                 Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
               Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -47,15 +47,13 @@
         val offset = snapshot.revert(buffer_offset)
         snapshot.node.command_at(offset) match {
           case Some((command, command_start)) =>
-            val root_node =
-              Markup_Tree.Node[Hyperlink]((Text.Range(offset) - command_start), null)
-
-            (snapshot.state(command).markup.select(root_node) {
-              case XML.Elem(Markup(Markup.ML_REF, _),
-                  List(XML.Elem(Markup(Markup.ML_DEF, props), _))) =>
+            val root = Text.Info[Hyperlink]((Text.Range(offset) - command_start), null)
+            (snapshot.state(command).markup.select(root) {
+              case Text.Info(_, XML.Elem(Markup(Markup.ML_REF, _),
+                  List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) =>
 //{{{
-                val node_range = root_node.range // FIXME proper range
-                val Text.Range(begin, end) = snapshot.convert(node_range + command_start)
+                val info_range = root.range // FIXME proper range
+                val Text.Range(begin, end) = snapshot.convert(info_range + command_start)
                 val line = buffer.getLineOfOffset(begin)
 
                 (Position.get_file(props), Position.get_line(props)) match {

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 22 16:43:20 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 22 18:46:16 2010 +0200
@@ -129,21 +129,21 @@
     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)((node: Markup_Tree.Node[Any]) =>
+      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 + "]"
             })
           })