misc tuning and clarification;
authorwenzelm
Sat Aug 07 13:19:48 2010 +0200 (2010-08-07)
changeset 38221e0f00f0945b4
parent 38220 b30aa2dbedca
child 38222 dac5fa0ac971
misc tuning and clarification;
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Pure/System/session.scala	Fri Aug 06 21:52:49 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Aug 07 13:19:48 2010 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  /*  Title:      Pure/System/session.scala
     1.5      Author:     Makarius
     1.6 +    Options:    :folding=explicit:collapseFolds=1:
     1.7  
     1.8  Isabelle session, potentially with running prover.
     1.9  */
    1.10 @@ -74,7 +75,7 @@
    1.11        case _ => None
    1.12      }
    1.13  
    1.14 -  private case class Start(timeout: Int, args: List[String])
    1.15 +  private case class Started(timeout: Int, args: List[String])
    1.16    private case object Stop
    1.17  
    1.18    private lazy val session_actor = actor {
    1.19 @@ -91,6 +92,7 @@
    1.20      /* document changes */
    1.21  
    1.22      def handle_change(change: Change)
    1.23 +    //{{{
    1.24      {
    1.25        require(change.parent.isDefined)
    1.26  
    1.27 @@ -120,6 +122,7 @@
    1.28        register_document(doc)
    1.29        prover.edit_document(change.parent.get.id, doc.id, id_edits)
    1.30      }
    1.31 +    //}}}
    1.32  
    1.33  
    1.34      /* prover results */
    1.35 @@ -130,6 +133,7 @@
    1.36      }
    1.37  
    1.38      def handle_result(result: Isabelle_Process.Result)
    1.39 +    //{{{
    1.40      {
    1.41        raw_results.event(result)
    1.42  
    1.43 @@ -175,6 +179,7 @@
    1.44        else if (!result.is_system)   // FIXME syslog (!?)
    1.45          bad_result(result)
    1.46      }
    1.47 +    //}}}
    1.48  
    1.49  
    1.50      /* prover startup */
    1.51 @@ -222,7 +227,7 @@
    1.52  
    1.53      loop {
    1.54        react {
    1.55 -        case Start(timeout, args) =>
    1.56 +        case Started(timeout, args) =>
    1.57            if (prover == null) {
    1.58              prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
    1.59              val origin = sender
    1.60 @@ -256,7 +261,9 @@
    1.61  
    1.62    /** buffered command changes -- delay_first discipline **/
    1.63  
    1.64 -  private lazy val command_change_buffer = actor {
    1.65 +  private lazy val command_change_buffer = actor
    1.66 +  //{{{
    1.67 +  {
    1.68      import scala.compat.Platform.currentTime
    1.69  
    1.70      var changed: Set[Command] = Set()
    1.71 @@ -292,6 +299,7 @@
    1.72        }
    1.73      }
    1.74    }
    1.75 +  //}}}
    1.76  
    1.77    def indicate_command_change(command: Command)
    1.78    {
    1.79 @@ -301,9 +309,10 @@
    1.80  
    1.81    /* main methods */
    1.82  
    1.83 -  def start(timeout: Int, args: List[String]): Option[String] =
    1.84 -    (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
    1.85 +  def started(timeout: Int, args: List[String]): Option[String] =
    1.86 +    (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
    1.87  
    1.88    def stop() { session_actor ! Stop }
    1.89 +
    1.90    def input(change: Change) { session_actor ! change }
    1.91  }
     2.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Aug 06 21:52:49 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Aug 07 13:19:48 2010 +0200
     2.3 @@ -1,6 +1,4 @@
     2.4  /*  Title:      Tools/jEdit/src/jedit/plugin.scala
     2.5 -    Author:     Johannes Hölzl, TU Munich
     2.6 -    Author:     Fabian Immler, TU Munich
     2.7      Author:     Makarius
     2.8  
     2.9  Main Isabelle/jEdit plugin setup.
    2.10 @@ -32,11 +30,6 @@
    2.11    var session: Session = null
    2.12  
    2.13  
    2.14 -  /* name */
    2.15 -
    2.16 -  val NAME = "Isabelle"
    2.17 -
    2.18 -
    2.19    /* properties */
    2.20  
    2.21    val OPTION_PREFIX = "options.isabelle."
    2.22 @@ -110,7 +103,7 @@
    2.23    }
    2.24  
    2.25  
    2.26 -  /* main jEdit components */  // FIXME ownership!?
    2.27 +  /* main jEdit components */
    2.28  
    2.29    def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    2.30  
    2.31 @@ -149,12 +142,12 @@
    2.32      }
    2.33  
    2.34  
    2.35 -  /* manage prover */
    2.36 +  /* manage prover */  // FIXME async!?
    2.37  
    2.38    private def prover_started(view: View): Boolean =
    2.39    {
    2.40      val timeout = Int_Property("startup-timeout") max 1000
    2.41 -    session.start(timeout, Isabelle.isabelle_args()) match {
    2.42 +    session.started(timeout, Isabelle.isabelle_args()) match {
    2.43        case Some(err) =>
    2.44          val text = new JTextArea(err); text.setEditable(false)
    2.45          Library.error_dialog(view, null, "Failed to start Isabelle process", text)