main session actor as independent thread, to avoid starvation via regular worker pool;
tuned;

--- a/src/Pure/System/session.scala	Mon Aug 23 16:50:09 2010 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 23 16:53:22 2010 +0200
@@ -69,8 +69,8 @@
   private case class Started(timeout: Int, args: List[String])
   private case object Stop
 
-  private lazy val session_actor = actor {
-
+  private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
+  {
     var prover: Isabelle_Process with Isar_Document = null
 
 
@@ -199,8 +199,9 @@
 
     /* main loop */
 
-    loop {
-      react {
+    var finished = false
+    while (!finished) {
+      receive {
         case Started(timeout, args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -211,10 +212,11 @@
           }
           else reply(None)
 
-        case Stop =>  // FIXME clarify; synchronous
+        case Stop => // FIXME synchronous!?
           if (prover != null) {
             prover.kill
             prover = null
+            finished = true
           }
 
         case change: Document.Change if prover != null =>
@@ -235,7 +237,7 @@
 
   /** buffered command changes (delay_first discipline) **/
 
-  private lazy val command_change_buffer = actor
+  private val command_change_buffer = actor
   //{{{
   {
     import scala.compat.Platform.currentTime
@@ -286,36 +288,33 @@
 
   private case class Edit_Version(edits: List[Document.Node_Text_Edit])
 
-  private val editor_history = new Actor
-  {
-    @volatile private var history = Document.History.init
+  @volatile private var history = Document.History.init
 
-    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
-      history.snapshot(name, pending_edits, current_state())
+  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+    history.snapshot(name, pending_edits, current_state())
 
-    def act
-    {
-      loop {
-        react {
-          case Edit_Version(edits) =>
-            val prev = history.tip.current
-            val result =
-              isabelle.Future.fork {
-                val previous = prev.join
-                val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
-                Thy_Syntax.text_edits(Session.this, previous, edits)
-              }
-            val change = new Document.Change(prev, edits, result)
-            history += change
-            change.current.map(_ => session_actor ! change)
-            reply(())
+  private val editor_history = actor
+  {
+    loop {
+      react {
+        case Edit_Version(edits) =>
+          val prev = history.tip.current
+          val result =
+            // FIXME potential denial-of-service concerning worker pool (!?!?)
+            isabelle.Future.fork {
+              val previous = prev.join
+              val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
+              Thy_Syntax.text_edits(Session.this, previous, edits)
+            }
+          val change = new Document.Change(prev, edits, result)
+          history += change
+          change.current.map(_ => session_actor ! change)
+          reply(())
 
-          case bad => System.err.println("editor_model: ignoring bad message " + bad)
-        }
+        case bad => System.err.println("editor_model: ignoring bad message " + bad)
       }
     }
   }
-  editor_history.start
 
 
 
@@ -326,8 +325,5 @@
 
   def stop() { session_actor ! Stop }
 
-  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
-    editor_history.snapshot(name, pending_edits)
-
   def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
 }