# HG changeset patch
# User wenzelm
# Date 1489588755 -3600
# Node ID c97abf0fa0c12f5b3882bec0d0bed0ea29fe6133
# Parent  0fe4ebab9fdfaeb66ec477db0e32b9460a97ed98
strict initialization of plugin.session: no user errors to be expected before session.start;

diff -r 0fe4ebab9fdf -r c97abf0fa0c1 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 14:29:55 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 15:39:15 2017 +0100
@@ -33,8 +33,7 @@
 
   def options: JEdit_Options = plugin.options
   def resources: JEdit_Resources = plugin.resources
-
-  @volatile var session: Session = new Session(JEdit_Resources.empty)
+  def session: Session = plugin.session
 
 
   /* semantic document content */
@@ -85,6 +84,22 @@
   def resources: JEdit_Resources = _resources
 
 
+  /* session */
+
+  private var _session: Session = null
+  private def init_session()
+  {
+    _session =
+      new Session(resources) {
+        override def output_delay = options.seconds("editor_output_delay")
+        override def prune_delay = options.seconds("editor_prune_delay")
+        override def syslog_limit = options.int("editor_syslog_limit")
+        override def reparse_limit = options.int("editor_reparse_limit")
+      }
+  }
+  def session: Session = _session
+
+
   /* misc support */
 
   val completion_history = new Completion.History_Variable
@@ -95,7 +110,7 @@
 
   def options_changed()
   {
-    PIDE.session.global_options.post(Session.Global_Options(options.value))
+    session.global_options.post(Session.Global_Options(options.value))
     delay_load.invoke()
   }
 
@@ -136,7 +151,7 @@
             if (options.bool("jedit_auto_resolve")) {
               val stable_tip_version =
                 if (models.forall(p => p._2.is_stable))
-                  PIDE.session.current_state().stable_tip_version
+                  session.current_state().stable_tip_version
                 else None
               stable_tip_version match {
                 case Some(version) => resources.undefined_blobs(version.nodes)
@@ -158,7 +173,7 @@
 
               GUI_Thread.later {
                 try {
-                  Document_Model.provide_files(PIDE.session, loaded_files)
+                  Document_Model.provide_files(session, loaded_files)
                   delay_init.invoke()
                 }
                 finally { delay_load_active.change(_ => false) }
@@ -189,11 +204,11 @@
     case Session.Terminated(_) =>
       GUI_Thread.later {
         GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
-          "Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content()))
+          "Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
       }
 
     case Session.Ready =>
-      PIDE.session.update_options(options.value)
+      session.update_options(options.value)
       init_models()
 
       if (!Isabelle.continuous_checking) {
@@ -248,7 +263,7 @@
         if (buffer.isLoaded) {
           JEdit_Lib.buffer_lock(buffer) {
             val node_name = resources.node_name(buffer)
-            val model = Document_Model.init(PIDE.session, node_name, buffer)
+            val model = Document_Model.init(session, node_name, buffer)
             for {
               text_area <- JEdit_Lib.jedit_text_areas(buffer)
               if Document_View.get(text_area).map(_.model) != Some(model)
@@ -327,7 +342,7 @@
 
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
-          if (PIDE.session.is_ready) {
+          if (session.is_ready) {
             delay_init.invoke()
             delay_load.invoke()
           }
@@ -344,7 +359,7 @@
           if (buffer != null && text_area != null) {
             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
                 msg.getWhat == EditPaneUpdate.CREATED) {
-              if (PIDE.session.is_ready)
+              if (session.is_ready)
                 init_view(buffer, text_area)
             }
             else {
@@ -370,7 +385,7 @@
           }
 
           spell_checker.update(options.value)
-          PIDE.session.update_options(options.value)
+          session.update_options(options.value)
 
         case _ =>
       }
@@ -414,6 +429,7 @@
 
     init_options()
     init_resources()
+    init_session()
     PIDE._plugin = this
 
     jEdit.setProperty("plugin-error.start-error", orig_plugin_error)
@@ -429,14 +445,6 @@
       init_mode_provider()
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
-      PIDE.session.stop()
-      PIDE.session = new Session(resources) {
-        override def output_delay = options.seconds("editor_output_delay")
-        override def prune_delay = options.seconds("editor_prune_delay")
-        override def syslog_limit = options.int("editor_syslog_limit")
-        override def reparse_limit = options.int("editor_reparse_limit")
-      }
-
       startup_failure = None
     }
     catch {
@@ -459,7 +467,7 @@
     }
 
     exit_models(JEdit_Lib.jedit_buffers().toList)
-    PIDE.session.stop()
+    session.stop()
     file_watcher.shutdown()
 
     PIDE._plugin = null