# HG changeset patch
# User wenzelm
# Date 1504273330 -7200
# Node ID d389714a8aaa124bb01878ce670cd88a042c11e4
# Parent  cc93f86e005fde8a6a617a62069fa4ef4d8052f3
clarified startup sequence;

diff -r cc93f86e005f -r d389714a8aaa src/Tools/jEdit/src-base/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)
   }
 
diff -r cc93f86e005f -r d389714a8aaa src/Tools/jEdit/src/plugin.scala
--- 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()