# HG changeset patch
# User immler@in.tum.de
# Date 1242992614 -7200
# Node ID 08f0d81c6833371b25a6f24910afa115f0fcbefe
# Parent  2adb23c3e5d1d0ac7198aad54ccb5973c0baa77c
reduced to one markup-tree

diff -r 2adb23c3e5d1 -r 08f0d81c6833 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri May 22 13:43:34 2009 +0200
@@ -33,7 +33,7 @@
     if (prover_setup.isDefined) {
         val document = prover_setup.get.prover.document
         for (command <- document.commands)
-          data.root.add(command.root_node.swing_node(document))
+          data.root.add(command.highlight_node.swing_node(document))
         
         if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     } else {
diff -r 2adb23c3e5d1 -r 08f0d81c6833 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:34 2009 +0200
@@ -53,10 +53,10 @@
     if (st == Command.Status.UNPROCESSED) {
       state_results.clear
       // delete markup
-      state_markup = empty_root_node
-      highlight_markup = empty_root_node
-      types_markup = empty_root_node
-      refs_markup = empty_root_node
+      markup_root.filter(_.kind match {
+          case MarkupNode.RootNode() | MarkupNode.OuterNode() => true
+          case _ => false
+        })
     }
     _status = st
   }
@@ -81,23 +81,22 @@
   /* markup */
 
   val empty_root_node =
-    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil, id, content, Markup.COMMAND_SPAN)
+    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil,
+                   id, content, Markup.COMMAND_SPAN, MarkupNode.RootNode())
 
-  var command_markup = empty_root_node
+  var markup_root = empty_root_node
 
-  var state_markup = empty_root_node
-  var highlight_markup = empty_root_node
-  var types_markup = empty_root_node
-  var refs_markup = empty_root_node
-  var state_markups = List(state_markup, highlight_markup, types_markup, refs_markup)
+  def highlight_node: MarkupNode = {
+    import MarkupNode._
+    markup_root.filter(_.kind match {
+      case RootNode() | OuterNode() | HighlightNode() => true
+      case _ => false
+    }).head
+  }
 
-  def highlight_node = (command_markup /: highlight_markup.children) (_ + _)
-
-  def root_node = (command_markup /: state_markup.children) (_ + _)
-
-  def markup_node(desc: String, begin: Int, end: Int) =
+  def markup_node(desc: String, begin: Int, end: Int, kind: MarkupNode.Kind) =
     new MarkupNode(this, begin, end, Nil, id,
                    if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
-                   desc)
+                   desc, kind)
 
 }
diff -r 2adb23c3e5d1 -r 08f0d81c6833 src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:34 2009 +0200
@@ -14,6 +14,12 @@
 import javax.swing.tree._
 
 object MarkupNode {
+  abstract class Kind
+  case class RootNode extends Kind
+  case class OuterNode extends Kind
+  case class HighlightNode extends Kind
+  case class TypeNode extends Kind
+  case class RefNode extends Kind
 
   def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
 
@@ -37,9 +43,10 @@
   }
 }
 
-class MarkupNode (val base : Command, val start : Int, val stop : Int,
+class MarkupNode (val base: Command, val start: Int, val stop: Int,
                   val children: List[MarkupNode],
-                  val id : String, val content : String, val desc : String) {
+                  val id: String, val content: String, val desc: String,
+                  val kind: MarkupNode.Kind) {
 
   def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
@@ -51,7 +58,7 @@
   def abs_stop(doc: ProofDocument) = base.start(doc) + stop
 
   def set_children(newchildren: List[MarkupNode]): MarkupNode =
-    new MarkupNode(base, start, stop, newchildren, id, content, desc)
+    new MarkupNode(base, start, stop, newchildren, id, content, desc, kind)
 
   def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
 
@@ -77,12 +84,12 @@
       val filled_gaps = for {
         child <- children
         markups = if (next_x < child.start) {
-          new MarkupNode(base, next_x, child.start, Nil, id, content, desc) :: child.flatten
+          new MarkupNode(base, next_x, child.start, Nil, id, content, desc, kind) :: child.flatten
         } else child.flatten
         update = (next_x = child.stop)
         markup <- markups
       } yield markup
-      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, desc)
+      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, desc, kind)
       else filled_gaps
     }
   }
diff -r 2adb23c3e5d1 -r 08f0d81c6833 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 13:43:34 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 13:43:34 2009 +0200
@@ -188,18 +188,15 @@
                     kind match {
                       case Markup.ML_TYPING =>
                         val info = body.first.asInstanceOf[XML.Text].content
-                        command.types_markup += command.markup_node(info, begin, end)
-                        command.state_markup += command.markup_node(info, begin, end)
+                        command.markup_root += command.markup_node(info, begin, end, MarkupNode.TypeNode())
                       case Markup.ML_REF =>
-                        command.refs_markup += command.markup_node(body.toString, begin, end)
-                        command.state_markup += command.markup_node(body.toString, begin, end)
+                        command.markup_root += command.markup_node(body.toString, begin, end, MarkupNode.RefNode())
                       case kind =>
                         if (!running)
                           commands.get(markup_id).map (cmd =>
-                          cmd.command_markup += cmd.markup_node(kind, begin, end))
+                          cmd.markup_root += cmd.markup_node(kind, begin, end, MarkupNode.OuterNode()))
                         else {
-                          command.highlight_markup += command.markup_node(kind, begin, end)
-                          command.state_markup += command.markup_node(kind, begin, end)
+                          command.markup_root += command.markup_node(kind, begin, end, MarkupNode.HighlightNode())
                         }
                     }
                     command_change(command)