# HG changeset patch
# User wenzelm
# Date 1232456215 -3600
# Node ID 7985efd78aa1e5a570ea79f21a600608f685935a
# Parent  6475bfb4ff99c3725ed391de23852069668dec32
tuned handling of accumulated results;

diff -r 6475bfb4ff99 -r 7985efd78aa1 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Mon Jan 19 23:29:44 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jan 20 13:56:55 2009 +0100
@@ -69,7 +69,7 @@
         if (state == null)
           state_panel.setDocument(null: Document)
         else
-          state_panel.setDocument(state.results_xml, UserAgent.baseURL)
+          state_panel.setDocument(state.result_document, UserAgent.baseURL)
       }
     })
   
diff -r 6475bfb4ff99 -r 7985efd78aa1 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Jan 19 23:29:44 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 13:56:55 2009 +0100
@@ -11,6 +11,8 @@
 import javax.swing.text.Position
 import javax.swing.tree.DefaultMutableTreeNode
 
+import scala.collection.mutable.ListBuffer
+
 import isabelle.proofdocument.{Token, ProofDocument}
 import isabelle.jedit.{Isabelle, Plugin}
 import isabelle.XML
@@ -59,17 +61,15 @@
 
   /* accumulated results */
 
-  var results: List[XML.Tree] = Nil
+  private val results = new ListBuffer[XML.Tree]
+  def add_result(tree: XML.Tree) { results += tree }
 
-  def results_xml = XML.document(
-    results match {
+  def result_document = XML.document(
+    results.toList match {
       case Nil => XML.Elem("message", Nil, Nil)
       case List(elem) => elem
-      case _ => XML.Elem("messages", Nil, List(results.first, results.last))
+      case elems => XML.Elem("messages", Nil, List(elems.first, elems.last))  // FIXME all elems!?
     }, "style")
-  def add_result(tree: XML.Tree) {
-    results = results ::: List(tree)    // FIXME canonical reverse order
-  }
 
 
   /* content */