handle statuses in Command

--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala	Sun Dec 07 15:36:24 2008 +0100
@@ -40,7 +40,7 @@
       if (state == null)
         panel.setDocument(null : Document)
       else
-        panel.setDocument(state.document, UserAgent.baseURL)
+        panel.setDocument(state.results_xml, UserAgent.baseURL)
     })
   }
 }

--- a/src/Tools/jEdit/src/prover/Command.scala	Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Dec 07 15:36:24 2008 +0100
@@ -26,7 +26,7 @@
   def idFromString(id : String) = Long.unbox(java.lang.Long.valueOf(id, 36))
 }
 
-class Command(val first : Token[Command], val last : Token[Command]) {
+class Command(val document : Document, val first : Token[Command], val last : Token[Command]) {
   import Command._
   
   {
@@ -45,10 +45,10 @@
   //offsets relative to first.start!
   class Status(val kind : String,val start : Int, val stop : Int ) { }
   var statuses = Nil : List[Status]
-  def statusesxml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
+  def statuses_xml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
 
   def idString = java.lang.Long.toString(id, 36)
-  def document = XML.document(results match {
+  def results_xml = XML.document(results match {
                                 case Nil => XML.Elem("message", List(), List())
                                 case List(elem) => elem
                                 case _ =>
@@ -60,7 +60,7 @@
   }
   
   val root_node = {
-    val content = Plugin.plugin.prover.document.getContent(this)
+    val content = document.getContent(this)
     val ra = new RelativeAsset(this, 0, stop - start, "command", content)
     new DefaultMutableTreeNode(ra)
   }
@@ -99,26 +99,42 @@
   }
 
  def addStatus(tree : XML.Tree) {
-    val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
+    val (state, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
                                    case _ => null}
-
-    //process attributes:
-    var markup_begin = -1
-    var markup_end = -1
-    for((n, a) <- attr) {
-      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - 1
-      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - 1
-    }
-    if(markup_begin > -1 && markup_end > -1){
-      statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
-      val markup_content = content.substring(markup_begin, markup_end)
-      val asset = new RelativeAsset(this, markup_begin, markup_end, markup_info, markup_content)
-      val new_node = new DefaultMutableTreeNode(asset)
-      insert_node(new_node, root_node)
+    if (phase != Phase.REMOVED && phase != Phase.REMOVE) {
+      state match {
+        case "finished" =>
+          phase = Phase.FINISHED
+        case "unprocessed" =>
+          phase = Phase.UNPROCESSED
+        case "failed" =>
+          phase = Phase.FAILED
+        case "removed" =>
+          // TODO: never lose information on command + id ??
+          //document.prover.commands.removeKey(st.idString)
+          phase = Phase.REMOVED
+        case _ =>
+          //process attributes:
+          var markup_begin = -1
+          var markup_end = -1
+          for((n, a) <- attr) {
+            if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - 1
+            if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - 1
+          }
+          if(markup_begin > -1 && markup_end > -1){
+            statuses = new Status(state, markup_begin, markup_end) :: statuses
+            val markup_content = content.substring(markup_begin, markup_end)
+            val asset = new RelativeAsset(this, markup_begin, markup_end, state, markup_content)
+            val new_node = new DefaultMutableTreeNode(asset)
+            insert_node(new_node, root_node)
+          } else {
+            System.err.println("addStatus - ignored: " + tree)
+          }
+      }
     }
   }
 
-  def content = Plugin.plugin.prover.document.getContent(this)
+  def content = document.getContent(this)
 
   def next = if (last.next != null) last.next.command else null
   def previous = if (first.previous != null) first.previous.command else null

--- a/src/Tools/jEdit/src/prover/Document.scala	Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala	Sun Dec 07 15:36:24 2008 +0100
@@ -10,7 +10,7 @@
                         val removedCommands : List[Command])
 }
 
-class Document(text : Text, prover : Prover) extends ProofDocument[Command](text) 
+class Document(text : Text, val prover : Prover) extends ProofDocument[Command](text)
 { 
   val structuralChanges = new EventSource[Document.StructureChange]() 
   
@@ -117,7 +117,7 @@
       
       if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
         if (! overrun) {
-          addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
+          addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
           cmdStart = scan
           cmdStop = scan
         }
@@ -140,7 +140,7 @@
     }
     
     if (cmdStart != null)
-      addedCommands = new Command(cmdStart, cmdStop) :: addedCommands
+      addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
     
     // relink commands
     addedCommands = addedCommands.reverse

--- a/src/Tools/jEdit/src/prover/Prover.scala	Sun Dec 07 15:01:37 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Dec 07 15:36:24 2008 +0100
@@ -106,32 +106,7 @@
               
       case IsabelleProcess.Kind.STATUS =>
         st.addStatus(tree)
-        val state = tree match { case Elem("message", _,
-                                           Elem (name, _, _) :: _) => name
-                                 case _ => null }
-        
-        if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
-          state match {
-            case "finished" => 
-              st.phase = Phase.FINISHED
-              fireChange()
-              
-            case "unprocessed" => 
-              st.phase = Phase.UNPROCESSED
-              fireChange()
-                    
-            case "failed" => 
-              st.phase = Phase.FAILED
-              fireChange()
-                    
-            case "removed" =>
-              commands.removeKey(st.idString)
-              st.phase = Phase.REMOVED
-              fireChange()
-              
-            case _ =>
-          }
-        }
+        fireChange()
       case _ =>
     }
   }