clarified startup sequence;
authorwenzelm
Fri, 01 Sep 2017 15:42:10 +0200
changeset 66593 d389714a8aaa
parent 66592 cc93f86e005f
child 66594 c16ed3250de0
clarified startup sequence;
src/Tools/jEdit/src-base/plugin.scala
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Fri Sep 01 15:21:10 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Fri Sep 01 15:42:10 2017 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.EBPlugin
+import org.gjt.sp.jedit.{Debug, EBPlugin}
 import org.gjt.sp.util.SyntaxUtilities
 
 
@@ -19,6 +19,8 @@
   {
     Isabelle_System.init()
 
+    Debug.DISABLE_SEARCH_DIALOG_POOL = true
+
     SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
   }
 
--- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 01 15:21:10 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 01 15:42:10 2017 +0200
@@ -13,7 +13,7 @@
 
 import java.io.{File => JFile}
 
-import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.syntax.ModeProvider
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
@@ -414,9 +414,6 @@
 
   override def start()
   {
-    Debug.DISABLE_SEARCH_DIALOG_POOL = true
-
-
     /* strict initialization */
 
     init_options()