--- a/src/Pure/PIDE/batch_session.scala Tue Mar 14 11:48:15 2017 +0100
+++ b/src/Pure/PIDE/batch_session.scala Tue Mar 14 11:49:51 2017 +0100
@@ -38,8 +38,9 @@
val handler = new Build.Handler(progress, session)
- prover_session.phase_changed +=
- Session.Consumer[Session.Phase](getClass.getName) {
+ Isabelle_Process.start(prover_session, options, logic = parent_session,
+ phase_changed =
+ {
case Session.Ready =>
prover_session.add_protocol_handler(handler)
val master_dir = session_info.dir
@@ -51,9 +52,7 @@
case Session.Shutdown =>
batch_session.session_result.fulfill(())
case _ =>
- }
-
- Isabelle_Process.start(prover_session, options, logic = parent_session)
+ })
batch_session
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Mar 14 11:48:15 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Mar 14 11:49:51 2017 +0100
@@ -67,7 +67,8 @@
Isabelle_Process.start(PIDE.session, session_options(),
logic = session_name(), dirs = session_dirs(), modes = modes,
- store = Sessions.store(session_build_mode() == "system"))
+ store = Sessions.store(session_build_mode() == "system"),
+ phase_changed = PIDE.plugin.session_phase_changed)
}
def session_list(): List[String] =
--- a/src/Tools/jEdit/src/plugin.scala Tue Mar 14 11:48:15 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 14 11:49:51 2017 +0100
@@ -241,43 +241,43 @@
/* session phase */
- private val session_phase =
- Session.Consumer[Session.Phase](getClass.getName) {
- case Session.Terminated(_) =>
- GUI_Thread.later {
- GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
- "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
- }
+ val session_phase_changed: Session.Phase => Unit =
+ {
+ case Session.Terminated(_) =>
+ GUI_Thread.later {
+ GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
+ "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
+ }
- case Session.Ready =>
- PIDE.session.update_options(PIDE.options.value)
- PIDE.init_models()
+ case Session.Ready =>
+ PIDE.session.update_options(PIDE.options.value)
+ PIDE.init_models()
- if (!Isabelle.continuous_checking) {
- GUI_Thread.later {
- val answer =
- GUI.confirm_dialog(jEdit.getActiveView,
- "Continuous checking of PIDE document",
- JOptionPane.YES_NO_OPTION,
- "Continuous checking is presently disabled:",
- "editor buffers will remain inactive!",
- "Enable continuous checking now?")
- if (answer == 0) Isabelle.continuous_checking = true
- }
+ if (!Isabelle.continuous_checking) {
+ GUI_Thread.later {
+ val answer =
+ GUI.confirm_dialog(jEdit.getActiveView,
+ "Continuous checking of PIDE document",
+ JOptionPane.YES_NO_OPTION,
+ "Continuous checking is presently disabled:",
+ "editor buffers will remain inactive!",
+ "Enable continuous checking now?")
+ if (answer == 0) Isabelle.continuous_checking = true
}
+ }
- delay_load.invoke()
+ delay_load.invoke()
- case Session.Shutdown =>
- GUI_Thread.later {
- delay_load.revoke()
- delay_init.revoke()
- PIDE.editor.flush()
- PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
- }
+ case Session.Shutdown =>
+ GUI_Thread.later {
+ delay_load.revoke()
+ delay_init.revoke()
+ PIDE.editor.flush()
+ PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
+ }
- case _ =>
- }
+ case _ =>
+ }
/* main plugin plumbing */
@@ -400,7 +400,6 @@
override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}
- PIDE.session.phase_changed += session_phase
PIDE.startup_failure = None
}
catch {
@@ -420,7 +419,6 @@
PIDE.completion_history.value.save()
}
- PIDE.session.phase_changed -= session_phase
PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
PIDE.session.stop()
PIDE.file_watcher.shutdown()