# HG changeset patch
# User wenzelm
# Date 1281179988 -7200
# Node ID e0f00f0945b4046ff483025da68d20dea2e90d5e
# Parent  b30aa2dbedca05fbd427d7466a87febc2c17e56d
misc tuning and clarification;

diff -r b30aa2dbedca -r e0f00f0945b4 src/Pure/System/session.scala
--- 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 }
 }
diff -r b30aa2dbedca -r e0f00f0945b4 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Aug 06 21:52:49 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Aug 07 13:19:48 2010 +0200
@@ -1,6 +1,4 @@
 /*  Title:      Tools/jEdit/src/jedit/plugin.scala
-    Author:     Johannes Hölzl, TU Munich
-    Author:     Fabian Immler, TU Munich
     Author:     Makarius
 
 Main Isabelle/jEdit plugin setup.
@@ -32,11 +30,6 @@
   var session: Session = null
 
 
-  /* name */
-
-  val NAME = "Isabelle"
-
-
   /* properties */
 
   val OPTION_PREFIX = "options.isabelle."
@@ -110,7 +103,7 @@
   }
 
 
-  /* main jEdit components */  // FIXME ownership!?
+  /* main jEdit components */
 
   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
 
@@ -149,12 +142,12 @@
     }
 
 
-  /* manage prover */
+  /* manage prover */  // FIXME async!?
 
   private def prover_started(view: View): Boolean =
   {
     val timeout = Int_Property("startup-timeout") max 1000
-    session.start(timeout, Isabelle.isabelle_args()) match {
+    session.started(timeout, Isabelle.isabelle_args()) match {
       case Some(err) =>
         val text = new JTextArea(err); text.setEditable(false)
         Library.error_dialog(view, null, "Failed to start Isabelle process", text)