# HG changeset patch # User wenzelm # Date 1666965546 -7200 # Node ID 5309f1283d93c87836ba8e43b44b15de5b98e2ca # Parent f70fcdc4cb43d4bee5cffbb537517fc5ed381b77 clarified modules; diff -r f70fcdc4cb43 -r 5309f1283d93 etc/build.props --- 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 \ diff -r f70fcdc4cb43 -r 5309f1283d93 src/Tools/jEdit/jedit_main/plugin.props --- 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 diff -r f70fcdc4cb43 -r 5309f1283d93 src/Tools/jEdit/src/isabelle_options.scala --- 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) -} diff -r f70fcdc4cb43 -r 5309f1283d93 src/Tools/jEdit/src/jedit_options.scala --- 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) } } -