# HG changeset patch
# User wenzelm
# Date 1489694953 -3600
# Node ID e9f9f962828da4f768060529c5b1533376a7f5a3
# Parent  fa1a5efee2ecfb2732a5be7a1d9369b97918afc9
tuned;

diff -r fa1a5efee2ec -r e9f9f962828d src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Mar 16 12:00:40 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Mar 16 21:09:13 2017 +0100
@@ -23,19 +23,6 @@
 
 object PIDE
 {
-  /* plugin instance */
-
-  @volatile var _plugin: Plugin = null
-
-  def plugin: Plugin =
-    if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
-    else _plugin
-
-  def options: JEdit_Options = plugin.options
-  def resources: JEdit_Resources = plugin.resources
-  def session: Session = plugin.session
-
-
   /* semantic document content */
 
   def snapshot(view: View): Document.Snapshot = GUI_Thread.now
@@ -54,9 +41,21 @@
       case None => error("No document view for current text area")
     }
   }
+
+
+  /* plugin instance */
+
+  @volatile var _plugin: Plugin = null
+
+  def plugin: Plugin =
+    if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
+    else _plugin
+
+  def options: JEdit_Options = plugin.options
+  def resources: JEdit_Resources = plugin.resources
+  def session: Session = plugin.session
 }
 
-
 class Plugin extends EBPlugin
 {
   /* options */