# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID 5427df0f6bcb9a59400277251af562f8fdcabe60
# Parent  f9b71bcf2eb7e838ab7459eba178e368c212e2d8
trait Accumulator;
template for State accumulating results from prover

diff -r f9b71bcf2eb7 -r 5427df0f6bcb src/Tools/jEdit/src/prover/Command.scala
--- 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
 {
diff -r f9b71bcf2eb7 -r 5427df0f6bcb src/Tools/jEdit/src/prover/State.scala
--- /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
+}