# HG changeset patch
# User immler@in.tum.de
# Date 1240833785 -7200
# Node ID 7c001369956abb9e2c02c09044442fa3cb77fb0d
# Parent  7dc6c231da4065fc08f4c5197ef7e164f8d8da56
included information on ML status messages in Sidekick's status-window

diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Apr 22 17:35:49 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 27 14:03:05 2009 +0200
@@ -85,7 +85,7 @@
       markup <- command.root_node.flatten
       if(to(markup.abs_stop(document)) > start)
       if(to(markup.abs_start(document)) < stop)
-      byte = DynamicTokenMarker.choose_byte(markup.kind)
+      byte = DynamicTokenMarker.choose_byte(markup.desc)
       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) -
diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Apr 22 17:35:49 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 27 14:03:05 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.kind, text_area.getPainter.getStyles), true)
+            DynamicTokenMarker.choose_color(node.desc, text_area.getPainter.getStyles), true)
         }
       }
     }
diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Wed Apr 22 17:35:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Apr 27 14:03:05 2009 +0200
@@ -82,12 +82,12 @@
   val root_node =
     new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, Markup.COMMAND_SPAN, content)
 
-  def add_markup(kind: String, begin: Int, end: Int) = {
+  def add_markup(desc: String, begin: Int, end: Int) = {
     val markup_content = if (end <= content.length) content.substring(begin, end)
       else {
         System.err.println (root_node.stop, content, content.length, end)
         "wrong indices?"
       }
-    root_node insert new MarkupNode(this, begin, end, id, kind, markup_content)
+    root_node insert new MarkupNode(this, begin, end, id, markup_content, desc)
   }
 }
diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Apr 22 17:35:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Apr 27 14:03:05 2009 +0200
@@ -22,7 +22,7 @@
 
     object RelativeAsset extends IAsset {
       override def getIcon : Icon = null
-      override def getShortString : String = node.kind
+      override def getShortString : String = node.content
       override def getLongString : String = node.desc
       override def getName : String = node.id
       override def setName (name : String) = ()
@@ -30,7 +30,7 @@
       override def getStart : Position = node.abs_start(doc)
       override def setEnd(end : Position) = ()
       override def getEnd : Position = node.abs_stop(doc)
-      override def toString = node.id + ": " + node.kind + "[" + getStart + " - " + getEnd + "]"
+      override def toString = node.id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
     }
 
     new DefaultMutableTreeNode(RelativeAsset)
@@ -38,7 +38,7 @@
 }
 
 class MarkupNode (val base : Command, val start : Int, val stop : Int,
-                    val id : String, val kind : String, val desc : String) {
+                    val id : String, val content : String, val desc : String) {
 
   def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
     val node = MarkupNode.markup2default_node (this, base, doc)
@@ -83,12 +83,12 @@
       val filled_gaps = for {
         child <- children
         markups = if (next_x < child.start) {
-          new MarkupNode(base, next_x, child.start, id, kind, "") :: child.flatten
+          new MarkupNode(base, next_x, child.start, id, content, "") :: 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, id, kind, "")
+      if (next_x < stop) filled_gaps + new MarkupNode(base, next_x, stop, id, content, "")
       else filled_gaps
     }
   }
@@ -111,7 +111,7 @@
         this remove new_child.children
       }
     } else {
-      System.err.println("ignored nonfitting markup " + new_child.id + new_child.kind + new_child.desc
+      System.err.println("ignored nonfitting markup " + new_child.id + new_child.content + new_child.desc
                          + "(" +new_child.start + ", "+ new_child.stop + ")")
     }
   }
@@ -120,5 +120,5 @@
   def fitting_into(node : MarkupNode) = node.start <= this.start &&
     node.stop >= this.stop
 
-  override def toString = "([" + start + " - " + stop + "] " + id + "( " + kind + "): " + desc
+  override def toString = "([" + start + " - " + stop + "] " + id + "( " + content + "): " + desc
 }
diff -r 7dc6c231da40 -r 7c001369956a src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Apr 22 17:35:49 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 27 14:03:05 2009 +0200
@@ -98,6 +98,10 @@
   
   private def handle_result(result: IsabelleProcess.Result)
   {
+    // helper-function (move to XML?)
+    def get_attr(attributes: List[(String, String)], attr: String): Option[String] =
+      attributes.find(kv => kv._1 == attr).map(_._2)
+
     def command_change(c: Command) = this ! c
     val (running, command) =
       result.props.find(p => p._1 == Markup.ID) match {
@@ -176,13 +180,26 @@
                     output_info.event(result.toString)
                     command.status = Command.Status.FAILED
                     command_change(command)
-
+                  // ML typing
+                  case XML.Elem(Markup.ML_TYPING, attr, body) =>
+                    val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
+                    val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
+                    val markup_id = get_attr(attr, Markup.ID).get
+                    val info = body.first.asInstanceOf[XML.Text].content
+                    command.add_markup(info, begin, end)
+                    command_change(command)
+                  // ML references
+                  case XML.Elem(Markup.ML_REF, attr, body) =>
+                    val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
+                    val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
+                    val markup_id = get_attr(attr, Markup.ID).get
+                    command.add_markup(body.toString, begin, end)
+                    command_change(command)
                   // other markup
-                  case XML.Elem(kind,
-                      (Markup.OFFSET, offset) :: (Markup.END_OFFSET, end_offset) ::
-                           (Markup.ID, markup_id) :: _, _) =>
-                    val begin = offset.toInt - 1
-                    val end = end_offset.toInt - 1
+                  case XML.Elem(kind, attr, body) =>
+                    val begin = get_attr(attr, Markup.OFFSET).get.toInt - 1
+                    val end = get_attr(attr, Markup.END_OFFSET).get.toInt - 1
+                    val markup_id = get_attr(attr, Markup.ID).get
 
                     val cmd =  // FIXME proper command version!? running!?
                       // outer syntax: no id in props