simplified Session.Phase;
authorwenzelm
Thu Sep 23 22:04:18 2010 +0200 (2010-09-23)
changeset 3963326a28110ece5
parent 39632 6328e7a06f32
child 39634 4030a9ef9c5a
simplified Session.Phase;
slightly more robust session startup;
misc tuning;
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Pure/System/session.scala	Thu Sep 23 22:00:36 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Sep 23 22:04:18 2010 +0200
     1.3 @@ -24,11 +24,9 @@
     1.4  
     1.5    sealed abstract class Phase
     1.6    case object Inactive extends Phase
     1.7 -  case object Startup extends Phase
     1.8    case object Exit extends Phase
     1.9    case object Ready extends Phase
    1.10    case object Shutdown extends Phase
    1.11 -  case object Terminated extends Phase
    1.12  }
    1.13  
    1.14  
    1.15 @@ -126,7 +124,7 @@
    1.16  
    1.17    @volatile private var _phase: Session.Phase = Session.Inactive
    1.18    def phase = _phase
    1.19 -  def phase_=(new_phase: Session.Phase)
    1.20 +  private def phase_=(new_phase: Session.Phase)
    1.21    {
    1.22      val old_phase = _phase
    1.23      _phase = new_phase
    1.24 @@ -211,7 +209,10 @@
    1.25            if (result.is_syslog) {
    1.26              reverse_syslog ::= result.message
    1.27              if (result.is_ready) phase = Session.Ready
    1.28 -            else if (result.is_exit) phase = Session.Exit
    1.29 +            else if (result.is_exit) {
    1.30 +              phase = Session.Exit
    1.31 +              phase = Session.Inactive
    1.32 +            }
    1.33            }
    1.34            else if (result.is_stdout) { }
    1.35            else if (result.is_status) {
    1.36 @@ -259,14 +260,13 @@
    1.37          case result: Isabelle_Process.Result => handle_result(result)
    1.38  
    1.39          case Start(timeout, args) if prover == null =>
    1.40 -          phase = Session.Startup
    1.41            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
    1.42  
    1.43          case Stop if phase == Session.Ready =>
    1.44            global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.45            phase = Session.Shutdown
    1.46            prover.terminate
    1.47 -          phase = Session.Terminated
    1.48 +          phase = Session.Inactive
    1.49            finished = true
    1.50            reply(())
    1.51  
     2.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 22:00:36 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 22:04:18 2010 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4    Buffer, EditPane, ServiceManager, View}
     2.5  import org.gjt.sp.jedit.buffer.JEditBuffer
     2.6  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     2.7 -import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate}
     2.8 +import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     2.9  import org.gjt.sp.jedit.gui.DockableWindowManager
    2.10  
    2.11  import org.gjt.sp.util.Log
    2.12 @@ -210,16 +210,18 @@
    2.13  {
    2.14    /* session management */
    2.15  
    2.16 -  private def session_startup()
    2.17 +  private def start_session()
    2.18    {
    2.19 -    val timeout = Isabelle.Int_Property("startup-timeout") max 1000
    2.20 -    val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    2.21 -    val logic = {
    2.22 -      val logic = Isabelle.Property("logic")
    2.23 -      if (logic != null && logic != "") logic
    2.24 -      else Isabelle.default_logic()
    2.25 +    if (Isabelle.session.phase == Session.Inactive) {
    2.26 +      val timeout = Isabelle.Int_Property("startup-timeout") max 1000
    2.27 +      val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    2.28 +      val logic = {
    2.29 +        val logic = Isabelle.Property("logic")
    2.30 +        if (logic != null && logic != "") logic
    2.31 +        else Isabelle.default_logic()
    2.32 +      }
    2.33 +      Isabelle.session.start(timeout, modes ::: List(logic))
    2.34      }
    2.35 -    Isabelle.session.start(timeout, modes ::: List(logic))
    2.36    }
    2.37  
    2.38    private def activate_buffer(buffer: Buffer)
    2.39 @@ -228,9 +230,13 @@
    2.40        Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
    2.41          case None =>
    2.42          case Some((_, thy_name)) =>
    2.43 -          val model = Document_Model.init(Isabelle.session, buffer, thy_name)
    2.44 -          for (text_area <- Isabelle.jedit_text_areas(buffer))
    2.45 -            Document_View.init(model, text_area)
    2.46 +          if (Document_Model(buffer).isEmpty) {
    2.47 +            val model = Document_Model.init(Isabelle.session, buffer, thy_name)
    2.48 +            for (text_area <- Isabelle.jedit_text_areas(buffer)) {
    2.49 +              if (Document_View(text_area).isEmpty)
    2.50 +                Document_View.init(model, text_area)
    2.51 +            }
    2.52 +          }
    2.53        }
    2.54      }
    2.55    }
    2.56 @@ -239,25 +245,26 @@
    2.57    {
    2.58      Isabelle.swing_buffer_lock(buffer) {
    2.59        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
    2.60 -        if (Document_View(text_area).isDefined) Document_View.exit(text_area)
    2.61 +        if (Document_View(text_area).isDefined)
    2.62 +          Document_View.exit(text_area)
    2.63        }
    2.64 -      if (Document_Model(buffer).isDefined) Document_Model.exit(buffer)
    2.65 +      if (Document_Model(buffer).isDefined)
    2.66 +        Document_Model.exit(buffer)
    2.67      }
    2.68    }
    2.69  
    2.70 -  private val session_manager = Simple_Thread.actor("session_manager", daemon = true) {
    2.71 -    var finished = false
    2.72 -    while (!finished) {
    2.73 -      receive {
    2.74 -        case (Session.Startup, Session.Exit) =>
    2.75 +  private val session_manager = actor {
    2.76 +    loop {
    2.77 +      react {
    2.78 +        case (Session.Inactive, Session.Exit) =>
    2.79            val text = new scala.swing.TextArea(Isabelle.session.syslog())
    2.80            text.editable = false
    2.81            Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
    2.82 -          finished = true
    2.83  
    2.84          case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
    2.85          case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
    2.86 -        case (_, Session.Terminated) => finished = true
    2.87 +
    2.88 +        case _ =>
    2.89        }
    2.90      }
    2.91    }
    2.92 @@ -268,15 +275,16 @@
    2.93    override def handleMessage(message: EBMessage)
    2.94    {
    2.95      message match {
    2.96 -      case msg: ViewUpdate
    2.97 -        if msg.getWhat == ViewUpdate.ACTIVATED =>
    2.98 -        session_startup()
    2.99 +      case msg: EditorStarted => start_session()
   2.100  
   2.101        case msg: BufferUpdate
   2.102 -        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   2.103 -        Document_Model(msg.getBuffer) match {
   2.104 -          case Some(model) => model.refresh()
   2.105 -          case _ =>
   2.106 +      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   2.107 +        val buffer = msg.getBuffer
   2.108 +        Isabelle.swing_buffer_lock(buffer) {
   2.109 +          Document_Model(buffer) match {
   2.110 +            case None => // FIXME activate_buffer(buffer)
   2.111 +            case Some(model) => model.refresh()
   2.112 +          }
   2.113          }
   2.114  
   2.115        case msg: EditPaneUpdate =>
   2.116 @@ -321,13 +329,12 @@
   2.117      Isabelle.system = new Isabelle_System
   2.118      Isabelle.system.install_fonts()
   2.119      Isabelle.session = new Session(Isabelle.system)
   2.120 -    Isabelle.session.phase_changed += session_manager._2
   2.121 +    Isabelle.session.phase_changed += session_manager
   2.122    }
   2.123  
   2.124    override def stop()
   2.125    {
   2.126      Isabelle.session.stop()
   2.127 -    session_manager._1.join
   2.128 -    Isabelle.session.phase_changed -= session_manager._2
   2.129 +    Isabelle.session.phase_changed -= session_manager
   2.130    }
   2.131  }