src/Tools/jEdit/src/plugin.scala

--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:26:25 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:32:12 2017 +0100
@@ -49,63 +49,6 @@
   lazy val editor = new JEdit_Editor
 
 
-  /* document model and view */
-
-  def exit_models(buffers: List[Buffer])
-  {
-    GUI_Thread.now {
-      buffers.foreach(buffer =>
-        JEdit_Lib.buffer_lock(buffer) {
-          JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
-          Document_Model.exit(buffer)
-        })
-      }
-  }
-
-  def init_models()
-  {
-    GUI_Thread.now {
-      PIDE.editor.flush()
-
-      for {
-        buffer <- JEdit_Lib.jedit_buffers()
-        if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
-      } {
-        if (buffer.isLoaded) {
-          JEdit_Lib.buffer_lock(buffer) {
-            val node_name = resources.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)
-            } Document_View.init(model, text_area)
-          }
-        }
-        else if (plugin != null) plugin.delay_init.invoke()
-      }
-
-      PIDE.editor.invoke_generated()
-    }
-  }
-
-  def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
-    GUI_Thread.now {
-      JEdit_Lib.buffer_lock(buffer) {
-        Document_Model.get(buffer) match {
-          case Some(model) => Document_View.init(model, text_area)
-          case None =>
-        }
-      }
-    }
-
-  def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
-    GUI_Thread.now {
-      JEdit_Lib.buffer_lock(buffer) {
-        Document_View.exit(text_area)
-      }
-    }
-
-
   /* current document content */
 
   def snapshot(view: View): Document.Snapshot = GUI_Thread.now
@@ -169,7 +112,7 @@
   lazy val delay_init =
     GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     {
-      PIDE.init_models()
+      init_models()
     }
 
   private val delay_load_active = Synchronized(false)
@@ -253,7 +196,7 @@
 
     case Session.Ready =>
       PIDE.session.update_options(PIDE.options.value)
-      PIDE.init_models()
+      init_models()
 
       if (!Isabelle.continuous_checking) {
         GUI_Thread.later {
@@ -275,13 +218,70 @@
         delay_load.revoke()
         delay_init.revoke()
         PIDE.editor.flush()
-        PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
+        exit_models(JEdit_Lib.jedit_buffers().toList)
       }
 
     case _ =>
   }
 
 
+  /* document model and view */
+
+  def exit_models(buffers: List[Buffer])
+  {
+    GUI_Thread.now {
+      buffers.foreach(buffer =>
+        JEdit_Lib.buffer_lock(buffer) {
+          JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
+          Document_Model.exit(buffer)
+        })
+      }
+  }
+
+  def init_models()
+  {
+    GUI_Thread.now {
+      PIDE.editor.flush()
+
+      for {
+        buffer <- JEdit_Lib.jedit_buffers()
+        if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
+      } {
+        if (buffer.isLoaded) {
+          JEdit_Lib.buffer_lock(buffer) {
+            val node_name = PIDE.resources.node_name(buffer)
+            val model = Document_Model.init(PIDE.session, node_name, buffer)
+            for {
+              text_area <- JEdit_Lib.jedit_text_areas(buffer)
+              if Document_View.get(text_area).map(_.model) != Some(model)
+            } Document_View.init(model, text_area)
+          }
+        }
+        else delay_init.invoke()
+      }
+
+      PIDE.editor.invoke_generated()
+    }
+  }
+
+  def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
+    GUI_Thread.now {
+      JEdit_Lib.buffer_lock(buffer) {
+        Document_Model.get(buffer) match {
+          case Some(model) => Document_View.init(model, text_area)
+          case None =>
+        }
+      }
+    }
+
+  def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
+    GUI_Thread.now {
+      JEdit_Lib.buffer_lock(buffer) {
+        Document_View.exit(text_area)
+      }
+    }
+
+
   /* main plugin plumbing */
 
   @volatile private var startup_failure: Option[Throwable] = None
@@ -323,7 +323,7 @@
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
           if (msg.getBuffer != null) {
-            PIDE.exit_models(List(msg.getBuffer))
+            exit_models(List(msg.getBuffer))
             PIDE.editor.invoke_generated()
           }
 
@@ -347,11 +347,11 @@
             if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
                 msg.getWhat == EditPaneUpdate.CREATED) {
               if (PIDE.session.is_ready)
-                PIDE.init_view(buffer, text_area)
+                init_view(buffer, text_area)
             }
             else {
               Isabelle.dismissed_popups(text_area.getView)
-              PIDE.exit_view(buffer, text_area)
+              exit_view(buffer, text_area)
             }
 
             if (msg.getWhat == EditPaneUpdate.CREATED)
@@ -368,7 +368,7 @@
           } {
             val buffer = edit_pane.getBuffer
             val text_area = edit_pane.getTextArea
-            if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
+            if (buffer != null && text_area != null) init_view(buffer, text_area)
           }
 
           spell_checker.update(PIDE.options.value)
@@ -422,7 +422,7 @@
       completion_history.value.save()
     }
 
-    PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
+    exit_models(JEdit_Lib.jedit_buffers().toList)
     PIDE.session.stop()
     PIDE.file_watcher.shutdown()
   }