eliminated ProverEvents.Activate -- handle "ready" within Prover;
tuned prover setup;
tuned;

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Sep 07 13:52:36 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Sep 07 21:09:26 2009 +0200
@@ -12,7 +12,7 @@
 import scala.collection.mutable
 
 import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
-import isabelle.prover.{Prover, ProverEvents, Command}
+import isabelle.prover.{Prover, Command}
 
 import java.awt.{Color, Graphics2D}
 import javax.swing.event.{CaretListener, CaretEvent}
@@ -39,20 +39,43 @@
 class TheoryView(text_area: JEditTextArea)
   extends TextAreaExtension with BufferListener
 {
-  
   val buffer = text_area.getBuffer
 
-  // start prover
+
+  /* prover setup */
+
+  val change_receiver: Actor = new Actor {
+    def act() {
+      loop {
+        react {
+          case c: Command =>
+            actor { Isabelle.plugin.command_change.event(c) }
+            if (current_document().commands.contains(c))
+            Swing_Thread.later {
+              // repaint if buffer is active
+              if (text_area.getBuffer == buffer) {
+                update_syntax(c)
+                invalidate_line(c)
+                phase_overview.repaint()
+              }
+            }
+          case d: ProofDocument =>
+            actor { Isabelle.plugin.document_change.event(d) }
+          case bad => System.err.println("change_receiver: ignoring bad message " + bad)
+        }
+      }
+    }
+  }
+
   val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic(), change_receiver)
-  prover.start() // start actor
-
+  
 
   /* activation */
 
   private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current)
 
   private val selected_state_controller = new CaretListener {
-    override def caretUpdate(e: CaretEvent) = {
+    override def caretUpdate(e: CaretEvent) {
       val doc = current_document()
       doc.command_at(e.getDot) match {
         case Some(cmd)
@@ -300,32 +323,11 @@
   }
 
 
-  /* receiving from prover */
+  /* init */
 
-  lazy val change_receiver: Actor = actor {
-    loop {
-      react {
-        case ProverEvents.Activate =>   // FIXME !?
-          Swing_Thread.now {
-            edits.clear
-            edits += Insert(0, buffer.getText(0, buffer.getLength))
-            edits_delay()
-          }
-        case c: Command =>
-          actor{Isabelle.plugin.command_change.event(c)}
-          if(current_document().commands.contains(c))
-          Swing_Thread.later {
-            // repaint if buffer is active
-            if(text_area.getBuffer == buffer) {
-              update_syntax(c)
-              invalidate_line(c)
-              phase_overview.repaint()
-            }
-          }
-        case d: ProofDocument =>
-          actor{Isabelle.plugin.document_change.event(d)}
-        case x => System.err.println("warning: change_receiver ignored " + x)
-      }
-    }
-  }
+  change_receiver.start()
+  prover.start()
+
+  edits += Insert(0, buffer.getText(0, buffer.getLength))
+  edits_delay()
 }

--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Sep 07 13:52:36 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Sep 07 21:09:26 2009 +0200
@@ -18,12 +18,6 @@
 import isabelle.proofdocument.{ProofDocument, Change, Token}
 
 
-object ProverEvents
-{
-  case class Activate
-}
-
-
 class Prover(isabelle_system: Isabelle_System, logic: String, change_receiver: Actor)
   extends Actor
 {
@@ -58,8 +52,6 @@
   def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   def document(id: Isar_Document.Document_ID) = document_versions.find(_.id == id)
 
-  private var initialized = false
-
   
   /* outer syntax keywords */
 
@@ -94,6 +86,8 @@
   val output_text_view = new JTextArea
   output_info += (result => output_text_view.append(result.toString + "\n"))
 
+  private case object Ready
+
   private def handle_result(result: Isabelle_Process.Result)
   {
     val state =
@@ -125,10 +119,7 @@
                   keyword_decls += name
 
                 // process ready (after initialization)
-                case XML.Elem(Markup.READY, _, _)
-                if !initialized =>
-                  initialized = true
-                  change_receiver ! ProverEvents.Activate
+                case XML.Elem(Markup.READY, _, _) => this ! Ready
 
                 // document edits
                 case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
@@ -168,15 +159,17 @@
   }
 
   def act() {
+    var ready = false
     loop {
       react {
-        case change: Change =>
+        case Ready => ready = true
+        case change: Change if ready =>
           val old = document(change.parent.get.id).get
           val (doc, structure_change) = old.text_changed(change)
           document_versions ::= doc
           edit_document(old, doc, structure_change)
           change_receiver ! doc
-        case x => System.err.println("warning: ignored " + x)
+        case bad if ready => System.err.println("prover: ignoring bad message " + bad)
       }
     }
   }