src/Pure/System/session.scala
changeset 38221 e0f00f0945b4
parent 38150 67fc24df3721
child 38222 dac5fa0ac971
--- a/src/Pure/System/session.scala	Fri Aug 06 21:52:49 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 07 13:19:48 2010 +0200
@@ -1,5 +1,6 @@
 /*  Title:      Pure/System/session.scala
     Author:     Makarius
+    Options:    :folding=explicit:collapseFolds=1:
 
 Isabelle session, potentially with running prover.
 */
@@ -74,7 +75,7 @@
       case _ => None
     }
 
-  private case class Start(timeout: Int, args: List[String])
+  private case class Started(timeout: Int, args: List[String])
   private case object Stop
 
   private lazy val session_actor = actor {
@@ -91,6 +92,7 @@
     /* document changes */
 
     def handle_change(change: Change)
+    //{{{
     {
       require(change.parent.isDefined)
 
@@ -120,6 +122,7 @@
       register_document(doc)
       prover.edit_document(change.parent.get.id, doc.id, id_edits)
     }
+    //}}}
 
 
     /* prover results */
@@ -130,6 +133,7 @@
     }
 
     def handle_result(result: Isabelle_Process.Result)
+    //{{{
     {
       raw_results.event(result)
 
@@ -175,6 +179,7 @@
       else if (!result.is_system)   // FIXME syslog (!?)
         bad_result(result)
     }
+    //}}}
 
 
     /* prover startup */
@@ -222,7 +227,7 @@
 
     loop {
       react {
-        case Start(timeout, args) =>
+        case Started(timeout, args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
             val origin = sender
@@ -256,7 +261,9 @@
 
   /** buffered command changes -- delay_first discipline **/
 
-  private lazy val command_change_buffer = actor {
+  private lazy val command_change_buffer = actor
+  //{{{
+  {
     import scala.compat.Platform.currentTime
 
     var changed: Set[Command] = Set()
@@ -292,6 +299,7 @@
       }
     }
   }
+  //}}}
 
   def indicate_command_change(command: Command)
   {
@@ -301,9 +309,10 @@
 
   /* main methods */
 
-  def start(timeout: Int, args: List[String]): Option[String] =
-    (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
+  def started(timeout: Int, args: List[String]): Option[String] =
+    (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
 
   def stop() { session_actor ! Stop }
+
   def input(change: Change) { session_actor ! change }
 }