# HG changeset patch
# User wenzelm
# Date 1253189754 -7200
# Node ID 7b8847852aaedb78d17a32ff3884147180e65121
# Parent  4431c498726d321eb8d0c72a88474db746198204
Prover: private Actor;

diff -r 4431c498726d -r 7b8847852aae src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Sep 16 22:01:11 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Sep 17 14:15:54 2009 +0200
@@ -71,7 +71,7 @@
     if (!edits.isEmpty) {
       val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
       _changes ::= change
-      prover ! change
+      prover.input(change)
       current_change = change
       edits.clear
     }
diff -r 4431c498726d -r 7b8847852aae src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Sep 16 22:01:11 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Thu Sep 17 14:15:54 2009 +0200
@@ -17,22 +17,26 @@
 import isabelle.proofdocument.{ProofDocument, Change, Token}
 
 
-class Prover(system: Isabelle_System, logic: String) extends Actor
+class Prover(system: Isabelle_System, logic: String)
 {
   /* incoming messages */
 
   private var prover_ready = false
 
-  def act() {
-    loop {
-      react {
-        case result: Isabelle_Process.Result => handle_result(result)
-        case change: Change if prover_ready => handle_change(change)
-        case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
+  private val receiver = new Actor {
+    def act() {
+      loop {
+        react {
+          case result: Isabelle_Process.Result => handle_result(result)
+          case change: Change if prover_ready => handle_change(change)
+          case bad if prover_ready => System.err.println("prover: ignoring bad message " + bad)
+        }
       }
     }
   }
 
+  def input(change: Change) { receiver ! change }
+
 
   /* outgoing messages */
 
@@ -43,9 +47,7 @@
   /* prover process */
 
   private val process =
-    new Isabelle_Process(system, this, "-m", "xsymbols", logic) with Isar_Document
-
-  def stop() { process.kill }
+    new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
 
 
   /* outer syntax keywords and completion */
@@ -110,7 +112,7 @@
                           val state = new Command_State(cmd)
                           states += (state_id -> state)
                           doc.states += (cmd -> state)
-                          command_change.event(cmd)
+                          command_change.event(cmd)   // FIXME really!?
                         case None =>
                       }
                     }
@@ -163,4 +165,11 @@
 
     document_change.event(doc)
   }
+
+
+  /* main controls */
+
+  def start() { receiver.start() }
+
+  def stop() { process.kill() }
 }