let MarkupNode carry arbitrary information

--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Fri May 22 13:43:35 2009 +0200
@@ -85,7 +85,7 @@
       markup <- command.highlight_node.flatten
       if(to(markup.abs_stop(document)) > start)
       if(to(markup.abs_start(document)) < stop)
-      byte = DynamicTokenMarker.choose_byte(markup.desc)
+      byte = DynamicTokenMarker.choose_byte(markup.info.toString)
       token_start = to(markup.abs_start(document)) - start max 0
       token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
                      (start - to(markup.abs_start(document)) max 0) -

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri May 22 13:43:35 2009 +0200
@@ -204,7 +204,7 @@
         val finish = to_current(node.abs_stop(document))
         if (finish > start && begin < end) {
           encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
-            DynamicTokenMarker.choose_color(node.desc, text_area.getPainter.getStyles), true)
+            DynamicTokenMarker.choose_color(node.info.toString, text_area.getPainter.getStyles), true)
         }
       }
     }

--- a/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri May 22 13:43:35 2009 +0200
@@ -53,8 +53,8 @@
     if (st == Command.Status.UNPROCESSED) {
       state_results.clear
       // delete markup
-      markup_root.filter(_.kind match {
-          case MarkupNode.RootNode() | MarkupNode.OuterNode() => true
+      markup_root.filter(_.info match {
+          case RootInfo() | OuterInfo(_) => true
           case _ => false
         })
     }
@@ -82,28 +82,28 @@
 
   val empty_root_node =
     new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, Nil,
-                   id, content, Markup.COMMAND_SPAN, MarkupNode.RootNode())
+                   id, content, RootInfo())
 
   var markup_root = empty_root_node
 
   def highlight_node: MarkupNode = {
     import MarkupNode._
-    markup_root.filter(_.kind match {
-      case RootNode() | OuterNode() | HighlightNode() => true
+    markup_root.filter(_.info match {
+      case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
       case _ => false
     }).head
   }
 
-  def markup_node(desc: String, begin: Int, end: Int, kind: MarkupNode.Kind) =
+  def markup_node(begin: Int, end: Int, info: MarkupInfo) =
     new MarkupNode(this, begin, end, Nil, id,
                    if (end <= content.length && begin >= 0) content.substring(begin, end) else "wrong indices??",
-                   desc, kind)
+                   info)
 
   def type_at(pos: Int): String = {
-    val types = markup_root.filter(_.kind match {case MarkupNode.TypeNode() => true case _ => false})
+    val types = markup_root.filter(_.info match {case TypeInfo(_) => true case _ => false})
     types.flatten(_.flatten).
       find(t => t.start <= pos && t.stop > pos).
-      map(t => "\"" + t.content + "\" : " + t.desc).
+      map(t => "\"" + t.content + "\" : " + (t.info match {case TypeInfo(i) => i case _ => ""})).
       getOrElse(null)
   }
 }

--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Fri May 22 13:43:35 2009 +0200
@@ -13,13 +13,14 @@
 import javax.swing.text.Position
 import javax.swing.tree._
 
+abstract class MarkupInfo
+case class RootInfo extends MarkupInfo
+case class OuterInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
+case class HighlightInfo(highlight: String) extends MarkupInfo {override def toString = highlight}
+case class TypeInfo(type_kind: String) extends MarkupInfo {override def toString = type_kind}
+case class RefInfo(info: Any) extends MarkupInfo {override def toString = info.toString}
+
 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 = {
 
@@ -29,7 +30,7 @@
     object RelativeAsset extends IAsset {
       override def getIcon : Icon = null
       override def getShortString : String = node.content
-      override def getLongString : String = node.desc
+      override def getLongString : String = node.info.toString
       override def getName : String = node.id
       override def setName (name : String) = ()
       override def setStart(start : Position) = ()
@@ -45,8 +46,7 @@
 
 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 kind: MarkupNode.Kind) {
+                  val id: String, val content: String, val info: Any) {
 
   def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
@@ -58,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, kind)
+    new MarkupNode(base, start, stop, newchildren, id, content, info)
 
   def add(child : MarkupNode) = set_children ((child :: children) sort ((a, b) => a.start < b.start))
 
@@ -84,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, kind) :: child.flatten
+          new MarkupNode(base, next_x, child.start, Nil, id, content, info) :: 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, kind)
+      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, Nil, id, content, info)
       else filled_gaps
     }
   }
@@ -111,7 +111,7 @@
       }
       else this set_children new_children
     } else {
-      error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
+      error("ignored nonfitting markup " + new_child.id + new_child.content + new_child.info.toString
                          + "(" +new_child.start + ", "+ new_child.stop + ")")
     }
   }
@@ -119,5 +119,5 @@
   // does this fit into node?
   def fitting_into(node : MarkupNode) = node.start <= this.start && node.stop >= this.stop
 
-  override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc
+  override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + info.toString
 }

--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 13:43:35 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri May 22 13:43:35 2009 +0200
@@ -188,15 +188,15 @@
                     kind match {
                       case Markup.ML_TYPING =>
                         val info = body.first.asInstanceOf[XML.Text].content
-                        command.markup_root += command.markup_node(info, begin, end, MarkupNode.TypeNode())
+                        command.markup_root += command.markup_node(begin, end, TypeInfo(info))
                       case Markup.ML_REF =>
-                        command.markup_root += command.markup_node(body.toString, begin, end, MarkupNode.RefNode())
+                        command.markup_root += command.markup_node(begin, end, RefInfo(body))
                       case kind =>
                         if (!running)
                           commands.get(markup_id).map (cmd =>
-                          cmd.markup_root += cmd.markup_node(kind, begin, end, MarkupNode.OuterNode()))
+                          cmd.markup_root += cmd.markup_node(begin, end, OuterInfo(kind)))
                         else {
-                          command.markup_root += command.markup_node(kind, begin, end, MarkupNode.HighlightNode())
+                          command.markup_root += command.markup_node(begin, end, HighlightInfo(kind))
                         }
                     }
                     command_change(command)