trait Accumulator;
template for State accumulating results from prover

--- a/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -19,6 +19,23 @@
 
 import sidekick.{SideKickParsedData, IAsset}
 
+trait Accumulator extends Actor
+{
+
+  start() // start actor
+
+  protected var _state: State
+  def state = _state
+
+  override def act() {
+    loop {
+      react {
+        case x: XML.Tree => _state += x
+      }
+    }
+  }
+}
+
 
 object Command
 {

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/prover/State.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -0,0 +1,12 @@
+/*
+ * Accumulating results from prover
+ *
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle.prover
+
+abstract class State
+{
+  def +(message: XML.Tree): State
+}