# HG changeset patch
# User wenzelm
# Date 1233090989 -3600
# Node ID 422a43b76f77228edbedca7e15f05a47b95a220d
# Parent  018bad916757efa104ee0fc313d7042acdb6b5c6
eliminated Command.Status.REMOVE/REMOVED;
added state_id;
refined add_result: running flag;

diff -r 018bad916757 -r 422a43b76f77 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 22:14:40 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 22:16:29 2009 +0100
@@ -24,8 +24,6 @@
   object Status extends Enumeration {
     val UNPROCESSED = Value("UNPROCESSED")
     val FINISHED = Value("FINISHED")
-    val REMOVE = Value("REMOVE")
-    val REMOVED = Value("REMOVED")
     val FAILED = Value("FAILED")
   }
 }
@@ -68,6 +66,8 @@
 
   /* command status */
 
+  var state_id: IsarDocument.State_ID = null
+
   private var _status = Command.Status.UNPROCESSED
   def status = _status
   def status_=(st: Command.Status.Value) {
@@ -84,10 +84,10 @@
   /* results */
 
   private val results = new mutable.ListBuffer[XML.Tree]
-  def add_result(tree: XML.Tree) { results += tree }
-
   private val state_results = new mutable.ListBuffer[XML.Tree]
-  def add_state_result(tree: XML.Tree) { state_results += tree }
+  def add_result(running: Boolean, tree: XML.Tree) {
+    (if (running) state_results else results) += tree
+  }
 
   def result_document = XML.document(
     results.toList ::: state_results.toList match {