--- a/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 17:18:45 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 18:06:30 2022 +0200
@@ -195,8 +195,7 @@
/* continuous checking */
- object continuous_checking
- extends JEdit_Options.Access(PIDE.options.bool, "editor_continuous_checking") {
+ object continuous_checking extends JEdit_Options.Bool_Access("editor_continuous_checking") {
override def changed(): Unit = {
super.changed()
PIDE.plugin.deps_changed()
@@ -210,15 +209,14 @@
}
}
- def set_continuous_checking(): Unit = continuous_checking.update(true)
- def reset_continuous_checking(): Unit = continuous_checking.update(false)
- def toggle_continuous_checking(): Unit = continuous_checking.change(b => !b)
+ def set_continuous_checking(): Unit = continuous_checking.set()
+ def reset_continuous_checking(): Unit = continuous_checking.reset()
+ def toggle_continuous_checking(): Unit = continuous_checking.toggle()
/* output state */
- object output_state
- extends JEdit_Options.Access(PIDE.options.bool, "editor_output_state") {
+ object output_state extends JEdit_Options.Bool_Access("editor_output_state") {
override def changed(): Unit = GUI_Thread.require {
super.changed()
PIDE.editor.flush_edits(hidden = true)
--- a/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 17:18:45 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 18:06:30 2022 +0200
@@ -39,6 +39,12 @@
}
def changed(): Unit = GUI_Thread.require { PIDE.session.update_options(access.options.value) }
}
+
+ class Bool_Access(name: String) extends Access(PIDE.options.bool, name) {
+ def set(): Unit = update(true)
+ def reset(): Unit = update(false)
+ def toggle(): Unit = change(b => !b)
+ }
}
class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
--- a/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 17:18:45 2022 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 18:06:30 2022 +0200
@@ -198,7 +198,7 @@
"Continuous checking is presently disabled:",
"editor buffers will remain inactive!",
"Enable continuous checking now?")
- if (answer == 0) Isabelle.set_continuous_checking()
+ if (answer == 0) Isabelle.continuous_checking.set()
}
}