sidekick root data: set buffer length to avoid crash of initial caret move;
separate Markup_Node, Markup_Tree, Markup_Text;
added Markup_Text.flatten;
Command.type_at: null-free version;
eliminated Command.RootInfo;
simplified printing of TypeInfo, RefInfo;
added Command.content(Int, Int);

--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Sep 06 22:27:32 2009 +0200
@@ -126,7 +126,7 @@
     while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
       val command = cmd.get
       for {
-        markup <- command.highlight_node(document).flatten
+        markup <- command.highlight(document).flatten
         command_start = command.start(document)
         abs_start = to(command_start + markup.start)
         abs_stop = to(command_start + markup.stop)

--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sun Sep 06 22:27:32 2009 +0200
@@ -18,7 +18,7 @@
 import errorlist.DefaultErrorSource
 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
 
-import isabelle.prover.{Command, MarkupNode}
+import isabelle.prover.{Command, Markup_Node}
 import isabelle.proofdocument.ProofDocument
 
 
@@ -31,26 +31,28 @@
 
   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   {
+    implicit def int_to_pos(offset: Int): Position =
+      new Position { def getOffset = offset; override def toString = offset.toString }
+
     stopped = false
 
     val data = new SideKickParsedData(buffer.getName)
+    val root = data.root
+    data.getAsset(root).setEnd(buffer.getLength)
 
     val prover_setup = Isabelle.prover_setup(buffer)
     if (prover_setup.isDefined) {
       val document = prover_setup.get.theory_view.current_document()
       for (command <- document.commands if !stopped) {
-        data.root.add(command.markup_root(document).
-          swing_tree((node: MarkupNode) =>
+        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
             {
-              implicit def int2pos(offset: Int): Position =
-                new Position { def getOffset = offset; override def toString = offset.toString }
-
+              val content = command.content(node.start, node.stop)
               val command_start = command.start(document)
               val id = command.id
 
               new DefaultMutableTreeNode(new IAsset {
                 override def getIcon: Icon = null
-                override def getShortString: String = node.content
+                override def getShortString: String = content
                 override def getLongString: String = node.info.toString
                 override def getName: String = id
                 override def setName(name: String) = ()
@@ -58,14 +60,13 @@
                 override def getStart: Position = command_start + node.start
                 override def setEnd(end: Position) = ()
                 override def getEnd: Position = command_start + node.stop
-                override def toString =
-                  id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
+                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
               })
             }))
       }
-      if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
+      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
     }
-    else data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
 
     data
   }

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 22:27:32 2009 +0200
@@ -293,7 +293,7 @@
     document.command_at(offset) match {
       case Some(cmd) =>
         document.token_start(cmd.tokens.first)
-        cmd.type_at(document, offset - cmd.start(document))
+        cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
       case None => null
     }
   }

--- a/src/Tools/jEdit/src/prover/Command.scala	Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Sep 06 22:27:32 2009 +0200
@@ -19,7 +19,6 @@
 
 trait Accumulator extends Actor
 {
-
   start() // start actor
 
   protected var _state: State
@@ -44,19 +43,16 @@
     val FAILED = Value("FAILED")
   }
 
-  case object RootInfo
   case class HighlightInfo(highlight: String) { override def toString = highlight }
-  case class TypeInfo(type_kind: String) { override def toString = type_kind }
+  case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
-    command_id: Option[String], offset: Option[Int]) {
-      override def toString = (file, line, command_id, offset).toString
-    }
+    command_id: Option[String], offset: Option[Int])
 }
 
 
 class Command(
-  val tokens: List[Token],
-  val starts: Map[Token, Int],
+    val tokens: List[Token],
+    val starts: Map[Token, Int],
   change_receiver: Actor) extends Accumulator
 {
   require(!tokens.isEmpty)
@@ -73,6 +69,7 @@
 
   val name = tokens.head.content
   val content: String = Token.string_from_tokens(tokens, starts)
+  def content(i: Int, j: Int): String = content.substring(i, j)
   val symbol_index = new Symbol.Index(content)
 
   def start(doc: ProofDocument) = doc.token_start(tokens.first)
@@ -85,15 +82,13 @@
 
   /* markup */
 
-  lazy val empty_root_node =
-    new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
-      content, Command.RootInfo, Nil)
+  lazy val empty_markup = new Markup_Text(Nil, content)
 
-  def markup_node(begin: Int, end: Int, info: Any): MarkupNode =
+  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
   {
     val start = symbol_index.decode(begin)
     val stop = symbol_index.decode(end)
-    new MarkupNode(start, stop, content.substring(start, stop), info, Nil)
+    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   }
 
 
@@ -106,7 +101,7 @@
   def status(doc: ProofDocument) = cmd_state(doc).state.status
   def result_document(doc: ProofDocument) = cmd_state(doc).result_document
   def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
-  def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
+  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
   def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
   def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
 }
@@ -124,13 +119,13 @@
         case elems => XML.Elem("messages", Nil, elems)
       }, "style")
 
-  def markup_root: MarkupNode =
-    (command.state.markup_root /: state.markup_root.children)(_ + _)
+  def markup_root: Markup_Text =
+    (command.state.markup_root /: state.markup_root.markup)(_ + _)
 
-  def type_at(pos: Int): String = state.type_at(pos)
+  def type_at(pos: Int): Option[String] = state.type_at(pos)
 
-  def ref_at(pos: Int): Option[MarkupNode] = state.ref_at(pos)
+  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
 
-  def highlight_node: MarkupNode =
-    (command.state.highlight_node /: state.highlight_node.children)(_ + _)
+  def highlight: Markup_Text =
+    (command.state.highlight /: state.highlight.markup)(_ + _)
 }
\ No newline at end of file

--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Sep 06 22:27:32 2009 +0200
@@ -12,78 +12,100 @@
 import isabelle.proofdocument.ProofDocument
 
 
-class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any,
-  val children: List[MarkupNode])
+class Markup_Node(val start: Int, val stop: Int, val info: Any)
 {
+  def fits_into(that: Markup_Node): Boolean =
+    that.start <= this.start && this.stop <= that.stop
+}
+
 
-  def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
-  {
-    val node = make_node(this)
-    children.foreach(node add _.swing_tree(make_node))
-    node
-  }
+class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
+{
+  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
 
-  def set_children(new_children: List[MarkupNode]): MarkupNode =
-    new MarkupNode(start, stop, content, info, new_children)
+  private def add(branch: Markup_Tree) =   // FIXME avoid sort
+    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
 
-  private def add(child: MarkupNode) =   // FIXME avoid sort?
-    set_children ((child :: children) sort ((a, b) => a.start < b.start))
-
-  def remove(nodes: List[MarkupNode]) = set_children(children -- nodes)
+  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
 
-  def fits_into(node: MarkupNode): Boolean =
-    node.start <= this.start && this.stop <= node.stop
-
-  def + (new_child: MarkupNode): MarkupNode =
+  def + (new_tree: Markup_Tree): Markup_Tree =
   {
-    if (new_child fits_into this) {
+    val new_node = new_tree.node
+    if (new_node fits_into node) {
       var inserted = false
-      val new_children =
-        children.map(c =>
-          if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
-          else c)
+      val new_branches =
+        branches.map(branch =>
+          if ((new_node fits_into branch.node) && !inserted) {
+            inserted = true
+            branch + new_tree
+          }
+          else branch)
       if (!inserted) {
-        // new_child did not fit into children of this
-        // -> insert new_child between this and its children
-        val fitting = children filter(_ fits_into new_child)
-        (this remove fitting) add ((new_child /: fitting) (_ + _))
+        // new_tree did not fit into children of this
+        // -> insert between this and its branches
+        val fitting = branches filter(_.node fits_into new_node)
+        (this remove fitting) add ((new_tree /: fitting)(_ + _))
       }
-      else this set_children new_children
+      else set_branches(new_branches)
     }
     else {
-      System.err.println("ignored nonfitting markup: " + new_child)
+      System.err.println("ignored nonfitting markup: " + new_node)
       this
     }
   }
 
-  def flatten: List[MarkupNode] = {
-    var next_x = start
-    if (children.isEmpty) List(this)
+  def flatten: List[Markup_Node] =
+  {
+    var next_x = node.start
+    if (branches.isEmpty) List(this.node)
     else {
-      val filled_gaps = for {
-        child <- children
-        markups =
-          if (next_x < child.start) {
-            // FIXME proper content!?
-            new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten
-          }
-          else child.flatten
-        update = (next_x = child.stop)
-        markup <- markups
-      } yield markup
-      if (next_x < stop)
-        filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!?
+      val filled_gaps =
+        for {
+          child <- branches
+          markups =
+            if (next_x < child.node.start)
+              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+            else child.flatten
+          update = (next_x = child.node.stop)
+          markup <- markups
+        } yield markup
+      if (next_x < node.stop)
+        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
       else filled_gaps
     }
   }
+}
 
-  def filter(p: MarkupNode => Boolean): List[MarkupNode] =
+
+class Markup_Text(val markup: List[Markup_Tree], val content: String)
+{
+  private lazy val root =
+    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+
+  def + (new_tree: Markup_Tree): Markup_Text =
+    new Markup_Text((root + new_tree).branches, content)
+
+  def filter(pred: Markup_Node => Boolean): Markup_Text =
   {
-    val filtered = children.flatMap(_.filter(p))
-    if (p(this)) List(this set_children(filtered))
-    else filtered
+    def filt(tree: Markup_Tree): List[Markup_Tree] =
+    {
+      val branches = tree.branches.flatMap(filt(_))
+      if (pred(tree.node)) List(tree.set_branches(branches))
+      else branches
+    }
+    new Markup_Text(markup.flatMap(filt(_)), content)
   }
 
-  override def toString =
-    "([" + start + " - " + stop + "] ( " + content + "): " + info.toString
+  def flatten: List[Markup_Node] = markup.flatten(_.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)
+  }
 }

--- a/src/Tools/jEdit/src/prover/State.scala	Sun Sep 06 16:21:01 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala	Sun Sep 06 22:27:32 2009 +0200
@@ -12,10 +12,10 @@
   val command: Command,
   val status: Command.Status.Value,
   rev_results: List[XML.Tree],
-  val markup_root: MarkupNode)
+  val markup_root: Markup_Text)
 {
   def this(command: Command) =
-    this(command, Command.Status.UNPROCESSED, Nil, command.empty_root_node)
+    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
 
 
   /* content */
@@ -26,42 +26,45 @@
   private def add_result(res: XML.Tree): State =
     new State(command, status, res :: rev_results, markup_root)
 
-  private def add_markup(markup: MarkupNode): State =
-    new State(command, status, rev_results, markup_root + markup)
+  private def add_markup(node: Markup_Tree): State =
+    new State(command, status, rev_results, markup_root + node)
 
   lazy val results = rev_results.reverse
 
 
   /* markup */
 
-  lazy val highlight_node: MarkupNode =
+  lazy val highlight: Markup_Text =
   {
     markup_root.filter(_.info match {
-      case Command.RootInfo | Command.HighlightInfo(_) => true
+      case Command.HighlightInfo(_) => true
       case _ => false
-    }).head
+    })
   }
 
-  private lazy val types =
+  private lazy val types: List[Markup_Node] =
     markup_root.filter(_.info match {
       case Command.TypeInfo(_) => true
-      case _ => false }).flatten(_.flatten)
+      case _ => false }).flatten
 
-  def type_at(pos: Int): String =
+  def type_at(pos: Int): Option[String] =
   {
-    types.find(t => t.start <= pos && pos < t.stop).map(t =>
-      t.content + ": " + (t.info match {
-        case Command.TypeInfo(i) => i
-        case _ => "" })).
-      getOrElse(null)
+    types.find(t => t.start <= pos && pos < t.stop) match {
+      case Some(t) =>
+        t.info match {
+          case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
+          case _ => None
+        }
+      case None => None
+    }
   }
 
-  private lazy val refs =
+  private lazy val refs: List[Markup_Node] =
     markup_root.filter(_.info match {
       case Command.RefInfo(_, _, _, _) => true
-      case _ => false }).flatten(_.flatten)
+      case _ => false }).flatten
 
-  def ref_at(pos: Int): Option[MarkupNode] =
+  def ref_at(pos: Int): Option[Markup_Node] =
     refs.find(t => t.start <= pos && pos < t.stop)