explicit Session.Phase indication with associated event bus;
authorwenzelm
Thu Sep 23 18:44:26 2010 +0200 (2010-09-23)
changeset 3963044181423183a
parent 39629 08eb2730a8a1
child 39631 cad7a5b7f641
explicit Session.Phase indication with associated event bus;
asynchronous Session.start();
synchronous Session.stop();
added Plugin.session_manager on top of basic Session;
eliminated separate isabelle.activate action;
misc tuning;
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/dist-template/properties/jedit.props
src/Tools/jEdit/plugin/Isabelle.props
src/Tools/jEdit/plugin/actions.xml
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Thu Sep 23 16:48:48 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Sep 23 18:44:26 2010 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  
     1.5  import scala.actors.Actor
     1.6  import Actor._
     1.7 -import scala.collection.mutable
     1.8  
     1.9  
    1.10  object Isabelle_Process
     2.1 --- a/src/Pure/System/session.scala	Thu Sep 23 16:48:48 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Sep 23 18:44:26 2010 +0200
     2.3 @@ -21,6 +21,14 @@
     2.4    case object Perspective
     2.5    case object Assignment
     2.6    case class Commands_Changed(set: Set[Command])
     2.7 +
     2.8 +  sealed abstract class Phase
     2.9 +  case object Inactive extends Phase
    2.10 +  case object Startup extends Phase
    2.11 +  case object Exit extends Phase
    2.12 +  case object Ready extends Phase
    2.13 +  case object Shutdown extends Phase
    2.14 +  case object Terminated extends Phase
    2.15  }
    2.16  
    2.17  
    2.18 @@ -40,6 +48,7 @@
    2.19  
    2.20    /* pervasive event buses */
    2.21  
    2.22 +  val phase_changed = new Event_Bus[(Session.Phase, Session.Phase)]
    2.23    val global_settings = new Event_Bus[Session.Global_Settings.type]
    2.24    val raw_messages = new Event_Bus[Isabelle_Process.Result]
    2.25    val commands_changed = new Event_Bus[Session.Commands_Changed]
    2.26 @@ -98,7 +107,7 @@
    2.27        receiveWithin(flush_timeout) {
    2.28          case command: Command => changed += command; invoke()
    2.29          case TIMEOUT => flush()
    2.30 -        case Stop => finished = true
    2.31 +        case Stop => finished = true; reply(())
    2.32          case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
    2.33        }
    2.34      }
    2.35 @@ -115,12 +124,21 @@
    2.36    @volatile private var reverse_syslog = List[XML.Elem]()
    2.37    def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
    2.38  
    2.39 +  @volatile private var _phase: Session.Phase = Session.Inactive
    2.40 +  def phase = _phase
    2.41 +  def phase_=(new_phase: Session.Phase)
    2.42 +  {
    2.43 +    val old_phase = _phase
    2.44 +    _phase = new_phase
    2.45 +    phase_changed.event(old_phase, new_phase)
    2.46 +  }
    2.47 +
    2.48    private val global_state = new Volatile(Document.State.init)
    2.49    def current_state(): Document.State = global_state.peek()
    2.50  
    2.51    private case object Interrupt_Prover
    2.52    private case class Edit_Version(edits: List[Document.Node_Text_Edit])
    2.53 -  private case class Started(timeout: Int, args: List[String])
    2.54 +  private case class Start(timeout: Int, args: List[String])
    2.55  
    2.56    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    2.57    {
    2.58 @@ -190,8 +208,11 @@
    2.59            }
    2.60            catch { case _: Document.State.Fail => bad_result(result) }
    2.61          case _ =>
    2.62 -          if (result.is_exit) prover = null  // FIXME ??
    2.63 -          else if (result.is_syslog) reverse_syslog ::= result.message
    2.64 +          if (result.is_syslog) {
    2.65 +            reverse_syslog ::= result.message
    2.66 +            if (result.is_ready) phase = Session.Ready
    2.67 +            else if (result.is_exit) phase = Session.Exit
    2.68 +          }
    2.69            else if (result.is_stdout) { }
    2.70            else if (result.is_status) {
    2.71              result.body match {
    2.72 @@ -213,46 +234,7 @@
    2.73      //}}}
    2.74  
    2.75  
    2.76 -    /* prover startup */
    2.77 -
    2.78 -    def startup_error(): String =
    2.79 -    {
    2.80 -      val buf = new StringBuilder
    2.81 -      while (
    2.82 -        receiveWithin(0) {
    2.83 -          case result: Isabelle_Process.Result =>
    2.84 -            if (result.is_system) {
    2.85 -              for (text <- XML.content(result.message))
    2.86 -                buf.append(text)
    2.87 -            }
    2.88 -            true
    2.89 -          case TIMEOUT => false
    2.90 -        }) {}
    2.91 -      buf.toString
    2.92 -    }
    2.93 -
    2.94 -    def prover_startup(timeout: Int): Option[String] =
    2.95 -    {
    2.96 -      receiveWithin(timeout) {
    2.97 -        case result: Isabelle_Process.Result if result.is_init =>
    2.98 -          handle_result(result)
    2.99 -          while (receive {
   2.100 -            case result: Isabelle_Process.Result =>
   2.101 -              handle_result(result); !result.is_ready
   2.102 -            }) {}
   2.103 -          None
   2.104 -
   2.105 -        case result: Isabelle_Process.Result if result.is_exit =>
   2.106 -          handle_result(result)
   2.107 -          Some(startup_error())
   2.108 -
   2.109 -        case TIMEOUT =>  // FIXME clarify
   2.110 -          prover.terminate; Some(startup_error())
   2.111 -      }
   2.112 -    }
   2.113 -
   2.114 -
   2.115 -    /* main loop */  // FIXME proper shutdown
   2.116 +    /* main loop */
   2.117  
   2.118      var finished = false
   2.119      while (!finished) {
   2.120 @@ -260,7 +242,7 @@
   2.121          case Interrupt_Prover =>
   2.122            if (prover != null) prover.interrupt
   2.123  
   2.124 -        case Edit_Version(edits) =>
   2.125 +        case Edit_Version(edits) if prover != null =>
   2.126            val previous = global_state.peek().history.tip.current
   2.127            val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
   2.128            val change = global_state.change_yield(_.extend_history(previous, edits, result))
   2.129 @@ -272,30 +254,21 @@
   2.130  
   2.131            reply(())
   2.132  
   2.133 -        case change: Document.Change if prover != null =>
   2.134 -          handle_change(change)
   2.135 +        case change: Document.Change if prover != null => handle_change(change)
   2.136 +
   2.137 +        case result: Isabelle_Process.Result => handle_result(result)
   2.138  
   2.139 -        case result: Isabelle_Process.Result =>
   2.140 -          handle_result(result)
   2.141 +        case Start(timeout, args) if prover == null =>
   2.142 +          phase = Session.Startup
   2.143 +          prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
   2.144  
   2.145 -        case Started(timeout, args) =>
   2.146 -          if (prover == null) {
   2.147 -            prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
   2.148 -            val origin = sender
   2.149 -            val opt_err = prover_startup(timeout + 500)
   2.150 -            if (opt_err.isDefined) prover = null
   2.151 -            origin ! opt_err
   2.152 -          }
   2.153 -          else reply(None)
   2.154 -
   2.155 -        case Stop => // FIXME synchronous!?
   2.156 -          if (prover != null) {
   2.157 -            global_state.change(_ => Document.State.init)
   2.158 -            prover.terminate
   2.159 -            prover = null
   2.160 -          }
   2.161 -
   2.162 -        case TIMEOUT =>  // FIXME clarify
   2.163 +        case Stop if phase == Session.Ready =>
   2.164 +          global_state.change(_ => Document.State.init)  // FIXME event bus!?
   2.165 +          phase = Session.Shutdown
   2.166 +          prover.terminate
   2.167 +          phase = Session.Terminated
   2.168 +          finished = true
   2.169 +          reply(())
   2.170  
   2.171          case bad if prover != null =>
   2.172            System.err.println("session_actor: ignoring bad message " + bad)
   2.173 @@ -307,10 +280,9 @@
   2.174  
   2.175    /** main methods **/
   2.176  
   2.177 -  def started(timeout: Int, args: List[String]): Option[String] =
   2.178 -    (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
   2.179 +  def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
   2.180  
   2.181 -  def stop() { command_change_buffer ! Stop; session_actor ! Stop }
   2.182 +  def stop() { command_change_buffer !? Stop; session_actor !? Stop }
   2.183  
   2.184    def interrupt() { session_actor ! Interrupt_Prover }
   2.185  
     3.1 --- a/src/Pure/Thy/thy_header.scala	Thu Sep 23 16:48:48 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Sep 23 18:44:26 2010 +0200
     3.3 @@ -32,11 +32,11 @@
     3.4    val Thy_Path1 = new Regex("([^/]*)\\.thy")
     3.5    val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy")
     3.6  
     3.7 -  def split_thy_path(path: String): (String, String) =
     3.8 +  def split_thy_path(path: String): Option[(String, String)] =
     3.9      path match {
    3.10 -      case Thy_Path1(name) => ("", name)
    3.11 -      case Thy_Path2(dir, name) => (dir, name)
    3.12 -      case _ => error("Bad theory file specification: " + path)
    3.13 +      case Thy_Path1(name) => Some(("", name))
    3.14 +      case Thy_Path2(dir, name) => Some((dir, name))
    3.15 +      case _ => None
    3.16      }
    3.17  }
    3.18  
     4.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Thu Sep 23 16:48:48 2010 +0200
     4.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Thu Sep 23 18:44:26 2010 +0200
     4.3 @@ -183,7 +183,6 @@
     4.4  isabelle-output.dock-position=bottom
     4.5  isabelle-raw-output.dock-position=bottom
     4.6  isabelle-session.dock-position=bottom
     4.7 -isabelle.activate.shortcut=CS+ENTER
     4.8  line-end.shortcut=END
     4.9  line-home.shortcut=HOME
    4.10  lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
     5.1 --- a/src/Tools/jEdit/plugin/Isabelle.props	Thu Sep 23 16:48:48 2010 +0200
     5.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props	Thu Sep 23 18:44:26 2010 +0200
     5.3 @@ -35,8 +35,7 @@
     5.4  
     5.5  #menu actions
     5.6  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
     5.7 -plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
     5.8 -isabelle.activate.label=Activate current buffer
     5.9 +plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.raw-output-panel isabelle.protocol-panel
    5.10  isabelle.session-panel.label=Prover Session panel
    5.11  isabelle.output-panel.label=Output panel
    5.12  isabelle.raw-output-panel.label=Raw Output panel
     6.1 --- a/src/Tools/jEdit/plugin/actions.xml	Thu Sep 23 16:48:48 2010 +0200
     6.2 +++ b/src/Tools/jEdit/plugin/actions.xml	Thu Sep 23 18:44:26 2010 +0200
     6.3 @@ -2,14 +2,6 @@
     6.4  <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
     6.5  
     6.6  <ACTIONS>
     6.7 -  <ACTION NAME="isabelle.activate">
     6.8 -		<CODE>
     6.9 -			isabelle.jedit.Isabelle.switch_active(view);
    6.10 -		</CODE>
    6.11 -		<IS_SELECTED>
    6.12 -			return isabelle.jedit.Isabelle.is_active(view);
    6.13 -		</IS_SELECTED>
    6.14 -	</ACTION>
    6.15  	<ACTION NAME="isabelle.session-panel">
    6.16  		<CODE>
    6.17  			wm.addDockableWindow("isabelle-session");
     7.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 16:48:48 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Sep 23 18:44:26 2010 +0200
     7.3 @@ -19,11 +19,14 @@
     7.4    Buffer, EditPane, ServiceManager, View}
     7.5  import org.gjt.sp.jedit.buffer.JEditBuffer
     7.6  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     7.7 -import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
     7.8 +import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate}
     7.9  import org.gjt.sp.jedit.gui.DockableWindowManager
    7.10  
    7.11  import org.gjt.sp.util.Log
    7.12  
    7.13 +import scala.actors.Actor
    7.14 +import Actor._
    7.15 +
    7.16  
    7.17  object Isabelle
    7.18  {
    7.19 @@ -115,7 +118,7 @@
    7.20    {
    7.21      val icon = GUIUtilities.loadIcon(name)
    7.22      if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
    7.23 -      Log.log(Log.ERROR, icon, "Bad icon: " + name);
    7.24 +      Log.log(Log.ERROR, icon, "Bad icon: " + name)
    7.25      icon
    7.26    }
    7.27  
    7.28 @@ -200,77 +203,76 @@
    7.29      }
    7.30      component
    7.31    }
    7.32 -
    7.33 -  def isabelle_args(): List[String] =
    7.34 -  {
    7.35 -    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    7.36 -    val logic = {
    7.37 -      val logic = Property("logic")
    7.38 -      if (logic != null && logic != "") logic
    7.39 -      else default_logic()
    7.40 -    }
    7.41 -    modes ++ List(logic)
    7.42 -  }
    7.43 -
    7.44 -
    7.45 -  /* manage prover */  // FIXME async!?
    7.46 -
    7.47 -  private def prover_started(view: View): Boolean =
    7.48 -  {
    7.49 -    val timeout = Int_Property("startup-timeout") max 1000
    7.50 -    session.started(timeout, Isabelle.isabelle_args()) match {
    7.51 -      case Some(err) =>
    7.52 -        val text = new scala.swing.TextArea(err)
    7.53 -        text.editable = false
    7.54 -        Library.error_dialog(view, null, "Failed to start Isabelle process", text)
    7.55 -        false
    7.56 -      case None => true
    7.57 -    }
    7.58 -  }
    7.59 -
    7.60 -
    7.61 -  /* activation */
    7.62 -
    7.63 -  def activate_buffer(view: View, buffer: Buffer)
    7.64 -  {
    7.65 -    if (prover_started(view)) {
    7.66 -      // FIXME proper error handling
    7.67 -      val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
    7.68 -
    7.69 -      val model = Document_Model.init(session, buffer, thy_name)
    7.70 -      for (text_area <- jedit_text_areas(buffer))
    7.71 -        Document_View.init(model, text_area)
    7.72 -    }
    7.73 -  }
    7.74 -
    7.75 -  def deactivate_buffer(buffer: Buffer)
    7.76 -  {
    7.77 -    session.stop()  // FIXME not yet
    7.78 -
    7.79 -    for (text_area <- jedit_text_areas(buffer))
    7.80 -      Document_View.exit(text_area)
    7.81 -    Document_Model.exit(buffer)
    7.82 -  }
    7.83 -
    7.84 -  def switch_active(view: View) =
    7.85 -  {
    7.86 -    val buffer = view.getBuffer
    7.87 -    if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
    7.88 -    else activate_buffer(view, buffer)
    7.89 -  }
    7.90 -
    7.91 -  def is_active(view: View): Boolean =
    7.92 -    Document_Model(view.getBuffer).isDefined
    7.93  }
    7.94  
    7.95  
    7.96  class Plugin extends EBPlugin
    7.97  {
    7.98 +  /* session management */
    7.99 +
   7.100 +  private def session_startup()
   7.101 +  {
   7.102 +    val timeout = Isabelle.Int_Property("startup-timeout") max 1000
   7.103 +    val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
   7.104 +    val logic = {
   7.105 +      val logic = Isabelle.Property("logic")
   7.106 +      if (logic != null && logic != "") logic
   7.107 +      else Isabelle.default_logic()
   7.108 +    }
   7.109 +    Isabelle.session.start(timeout, modes ::: List(logic))
   7.110 +  }
   7.111 +
   7.112 +  private def activate_buffer(buffer: Buffer)
   7.113 +  {
   7.114 +    Isabelle.swing_buffer_lock(buffer) {
   7.115 +      Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
   7.116 +        case None =>
   7.117 +        case Some((_, thy_name)) =>
   7.118 +          val model = Document_Model.init(Isabelle.session, buffer, thy_name)
   7.119 +          for (text_area <- Isabelle.jedit_text_areas(buffer))
   7.120 +            Document_View.init(model, text_area)
   7.121 +      }
   7.122 +    }
   7.123 +  }
   7.124 +
   7.125 +  private def deactivate_buffer(buffer: Buffer)
   7.126 +  {
   7.127 +    Isabelle.swing_buffer_lock(buffer) {
   7.128 +      for (text_area <- Isabelle.jedit_text_areas(buffer)) {
   7.129 +        if (Document_View(text_area).isDefined) Document_View.exit(text_area)
   7.130 +      }
   7.131 +      if (Document_Model(buffer).isDefined) Document_Model.exit(buffer)
   7.132 +    }
   7.133 +  }
   7.134 +
   7.135 +  private val session_manager = Simple_Thread.actor("session_manager", daemon = true) {
   7.136 +    var finished = false
   7.137 +    while (!finished) {
   7.138 +      receive {
   7.139 +        case (Session.Startup, Session.Exit) =>
   7.140 +          val text = new scala.swing.TextArea(Isabelle.session.syslog())
   7.141 +          text.editable = false
   7.142 +          // FIXME proper view!?
   7.143 +          Library.error_dialog(null, null, "Failed to start Isabelle process", text)
   7.144 +          finished = true
   7.145 +
   7.146 +        case (_, Session.Ready) => Isabelle.jedit_buffers.foreach(activate_buffer)
   7.147 +        case (_, Session.Shutdown) => Isabelle.jedit_buffers.foreach(deactivate_buffer)
   7.148 +        case (_, Session.Terminated) => finished = true
   7.149 +      }
   7.150 +    }
   7.151 +  }
   7.152 +
   7.153 +
   7.154    /* main plugin plumbing */
   7.155  
   7.156    override def handleMessage(message: EBMessage)
   7.157    {
   7.158      message match {
   7.159 +      case msg: ViewUpdate
   7.160 +        if msg.getWhat == ViewUpdate.ACTIVATED =>
   7.161 +        session_startup()
   7.162 +
   7.163        case msg: BufferUpdate
   7.164          if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   7.165          Document_Model(msg.getBuffer) match {
   7.166 @@ -304,12 +306,10 @@
   7.167  
   7.168        case msg: PropertiesChanged =>
   7.169          Swing_Thread.now {
   7.170 +          Isabelle.setup_tooltips()
   7.171            for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
   7.172              Document_View(text_area).get.extend_styles()
   7.173 -
   7.174 -          Isabelle.setup_tooltips()
   7.175          }
   7.176 -
   7.177          Isabelle.session.global_settings.event(Session.Global_Settings)
   7.178  
   7.179        case _ =>
   7.180 @@ -318,14 +318,17 @@
   7.181  
   7.182    override def start()
   7.183    {
   7.184 +    Isabelle.setup_tooltips()
   7.185      Isabelle.system = new Isabelle_System
   7.186      Isabelle.system.install_fonts()
   7.187      Isabelle.session = new Session(Isabelle.system)
   7.188 -    Isabelle.setup_tooltips()
   7.189 +    Isabelle.session.phase_changed += session_manager._2
   7.190    }
   7.191  
   7.192    override def stop()
   7.193    {
   7.194      Isabelle.session.stop()
   7.195 +    session_manager._1.join
   7.196 +    Isabelle.session.phase_changed -= session_manager._2
   7.197    }
   7.198  }