# HG changeset patch
# User wenzelm
# Date 1489488591 -3600
# Node ID 3b27169fd9da3aa0e6c5c55f8f9285f6d3411482
# Parent  ec9ec04546fc90c3810ca09bd5d709121ad0b26c
tuned;

diff -r ec9ec04546fc -r 3b27169fd9da src/Pure/PIDE/batch_session.scala
--- 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
   }
diff -r ec9ec04546fc -r 3b27169fd9da src/Tools/jEdit/src/jedit_sessions.scala
--- 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] =
diff -r ec9ec04546fc -r 3b27169fd9da src/Tools/jEdit/src/plugin.scala
--- 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()