clarified modules;
authorwenzelm
Fri, 28 Oct 2022 15:59:06 +0200
changeset 76390 5309f1283d93
parent 76389 f70fcdc4cb43
child 76391 6129e8cb140d
clarified modules;
etc/build.props
src/Tools/jEdit/jedit_main/plugin.props
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/jedit_options.scala
--- a/etc/build.props	Fri Oct 28 15:46:20 2022 +0200
+++ b/etc/build.props	Fri Oct 28 15:59:06 2022 +0200
@@ -251,7 +251,6 @@
   src/Tools/jEdit/src/isabelle.scala \
   src/Tools/jEdit/src/isabelle_encoding.scala \
   src/Tools/jEdit/src/isabelle_export.scala \
-  src/Tools/jEdit/src/isabelle_options.scala \
   src/Tools/jEdit/src/isabelle_session.scala \
   src/Tools/jEdit/src/isabelle_vfs.scala \
   src/Tools/jEdit/src/jedit_bibtex.scala \
--- a/src/Tools/jEdit/jedit_main/plugin.props	Fri Oct 28 15:46:20 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/plugin.props	Fri Oct 28 15:59:06 2022 +0200
@@ -23,9 +23,9 @@
 #options
 plugin.isabelle.jedit_main.Plugin.option-group=isabelle-general isabelle-rendering
 options.isabelle-general.label=General
-options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1();
+options.isabelle-general.code=new isabelle.jedit.JEdit_Options$Isabelle_General_Options();
 options.isabelle-rendering.label=Rendering
-options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
+options.isabelle-rendering.code=new isabelle.jedit.JEdit_Options$Isabelle_Rendering_Options();
 
 #menu actions and dockables
 plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle
--- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Oct 28 15:46:20 2022 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-/*  Title:      Tools/jEdit/src/isabelle_options.scala
-    Author:     Makarius
-
-Editor pane for plugin options.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
-
-
-abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
-  protected val components: List[(String, List[Option_Component])]
-
-  override def _init(): Unit = {
-    val dummy_property = "options.isabelle.dummy"
-
-    for ((s, cs) <- components) {
-      if (s.nonEmpty) {
-        jEdit.setProperty(dummy_property, s)
-        addSeparator(dummy_property)
-        jEdit.setProperty(dummy_property, null)
-      }
-      for (c <- cs) addComponent(c.title, c.peer)
-    }
-  }
-
-  override def _save(): Unit = {
-    for ((_, cs) <- components; c <- cs) c.save()
-  }
-}
-
-
-class Isabelle_Options1 extends Isabelle_Options("isabelle-general") {
-  val options: JEdit_Options = PIDE.options
-
-  private val predefined =
-    List(JEdit_Sessions.logic_selector(options),
-      JEdit_Spell_Checker.dictionaries_selector())
-
-  protected val components: List[(String, List[Option_Component])] =
-    options.make_components(predefined,
-      (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
-}
-
-
-class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") {
-  private val predefined =
-    (for {
-      (name, opt) <- PIDE.options.value.opt_iterator
-      if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
-    } yield PIDE.options.make_color_component(opt)).toList
-
-  assert(predefined.nonEmpty)
-
-  protected val components: List[(String, List[Option_Component])] =
-    PIDE.options.make_components(predefined, _ => false)
-}
--- a/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 15:46:20 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Oct 28 15:59:06 2022 +0200
@@ -16,6 +16,7 @@
 import scala.swing.{Component, CheckBox, TextArea}
 
 import org.gjt.sp.jedit.gui.ColorWellButton
+import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
 
 
 trait Option_Component extends Component {
@@ -81,6 +82,57 @@
       tooltip = "Output of proof state (normally shown on State panel)"
     }
   }
+
+
+  /* editor pane for plugin options */
+
+  abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) {
+    protected val components: List[(String, List[Option_Component])]
+
+    override def _init(): Unit = {
+      val dummy_property = "options.isabelle.dummy"
+
+      for ((s, cs) <- components) {
+        if (s.nonEmpty) {
+          jEdit.setProperty(dummy_property, s)
+          addSeparator(dummy_property)
+          jEdit.setProperty(dummy_property, null)
+        }
+        for (c <- cs) addComponent(c.title, c.peer)
+      }
+    }
+
+    override def _save(): Unit = {
+      for ((_, cs) <- components; c <- cs) c.save()
+    }
+  }
+
+
+  class Isabelle_General_Options extends Isabelle_Options("isabelle-general") {
+    val options: JEdit_Options = PIDE.options
+
+    private val predefined =
+      List(JEdit_Sessions.logic_selector(options),
+        JEdit_Spell_Checker.dictionaries_selector())
+
+    protected val components: List[(String, List[Option_Component])] =
+      options.make_components(predefined,
+        (for ((name, opt) <- options.value.opt_iterator if opt.public) yield name).toSet)
+  }
+
+
+  class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") {
+    private val predefined =
+      (for {
+        (name, opt) <- PIDE.options.value.opt_iterator
+        if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION)
+      } yield PIDE.options.make_color_component(opt)).toList
+
+    assert(predefined.nonEmpty)
+
+    protected val components: List[(String, List[Option_Component])] =
+      PIDE.options.make_components(predefined, _ => false)
+  }
 }
 
 class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
@@ -162,4 +214,3 @@
       .filterNot(_._2.isEmpty)
   }
 }
-