avoid deprecated PluginOptions with its unbounded window size;
authorwenzelm
Tue, 25 Aug 2015 16:49:14 +0200
changeset 61024 7b7f01afab71
parent 61023 46df28442a80
child 61025 636b578bfadd
avoid deprecated PluginOptions with its unbounded window size;
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Aug 25 13:46:24 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Aug 25 16:49:14 2015 +0200
@@ -19,7 +19,7 @@
 import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher}
 import org.gjt.sp.jedit.syntax.TokenMarker
 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
-import org.gjt.sp.jedit.options.PluginOptions
+import org.jedit.options.CombinedOptions
 
 
 object Isabelle
@@ -361,7 +361,7 @@
   def plugin_options(frame: Frame)
   {
     GUI_Thread.require {}
-    new org.gjt.sp.jedit.options.PluginOptions(frame, "plugin.isabelle.jedit.Plugin")
+    jEdit.setProperty("Plugin Options.last", "isabelle-general")
+    new CombinedOptions(frame, 1)
   }
 }
-
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 25 13:46:24 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 25 16:49:14 2015 +0200
@@ -14,7 +14,6 @@
 import scala.swing.{ListView, ScrollPane}
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
-import org.jedit.options.CombinedOptions
 import org.gjt.sp.jedit.gui.AboutDialog
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.buffer.JEditBuffer