# HG changeset patch
# User wenzelm
# Date 1440514154 -7200
# Node ID 7b7f01afab71214633d5dcffa343fcf52d8da5a0
# Parent  46df28442a800da0f57b7788ec258ce1b052dcca
avoid deprecated PluginOptions with its unbounded window size;

diff -r 46df28442a80 -r 7b7f01afab71 src/Tools/jEdit/src/isabelle.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)
   }
 }
-
diff -r 46df28442a80 -r 7b7f01afab71 src/Tools/jEdit/src/plugin.scala
--- 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