--- 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()