# HG changeset patch
# User wenzelm
# Date 1233076584 -3600
# Node ID 384427c750c8dc86cd09aa27131b4a75d91b71d5
# Parent  f084db5d20f1d7501ced8cee90e83708a0ddc681
state_results: separate buffer for messages from running command;
result_document: append all messages;
misc tuning;

diff -r f084db5d20f1 -r 384427c750c8 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 18:15:11 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 18:16:24 2009 +0100
@@ -34,7 +34,10 @@
 class Command(text: Text, val first: Token, val last: Token)
 {
   val id = Isabelle.plugin.id()
-  
+
+
+  /* content */
+
   {
     var t = first
     while (t != null) {
@@ -43,37 +46,6 @@
     }
   }
 
-
-  /* command status */
-
-  private var _status = Command.Status.UNPROCESSED
-  def status = _status
-  def status_=(st: Command.Status.Value) = {
-    if (st == Command.Status.UNPROCESSED) {
-      // delete markup
-      for (child <- root_node.children) {
-        child.children = Nil
-      }
-    }
-    _status = st
-  }
-
-
-  /* accumulated results */
-
-  private val results = new mutable.ListBuffer[XML.Tree]
-  def add_result(tree: XML.Tree) { results += tree }
-
-  def result_document = XML.document(
-    results.toList match {
-      case Nil => XML.Elem("message", Nil, Nil)
-      case List(elem) => elem
-      case elems => XML.Elem("messages", Nil, List(elems.first, elems.last))  // FIXME all elems!?
-    }, "style")
-
-
-  /* content */
-
   override def toString = name
 
   val name = text.content(first.start, first.stop)
@@ -94,7 +66,38 @@
   }
 
 
-  /* markup tree */
+  /* command status */
+
+  private var _status = Command.Status.UNPROCESSED
+  def status = _status
+  def status_=(st: Command.Status.Value) {
+    if (st == Command.Status.UNPROCESSED) {
+      // delete markup
+      for (child <- root_node.children) {
+        child.children = Nil
+      }
+    }
+    _status = st
+  }
+
+
+  /* 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 result_document = XML.document(
+    results.toList ::: state_results.toList match {
+      case Nil => XML.Elem("message", Nil, Nil)
+      case List(elem) => elem
+      case elems => XML.Elem("messages", Nil, elems)
+    }, "style")
+
+
+  /* markup */
 
   val root_node =
     new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)