--- a/src/Tools/jEdit/src/document_model.scala Sat Aug 13 18:06:30 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sat Aug 13 21:23:59 2022 +0200
@@ -342,7 +342,7 @@
): (Boolean, Document.Node.Perspective_Text) = {
GUI_Thread.require {}
- if (Isabelle.continuous_checking() && is_theory) {
+ if (JEdit_Options.continuous_checking() && is_theory) {
val snapshot = this.snapshot()
val reparse = snapshot.node.load_commands_changed(doc_blobs)
--- a/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 18:06:30 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 21:23:59 2022 +0200
@@ -195,41 +195,9 @@
/* continuous checking */
- object continuous_checking extends JEdit_Options.Bool_Access("editor_continuous_checking") {
- override def changed(): Unit = {
- super.changed()
- PIDE.plugin.deps_changed()
- }
-
- class GUI extends CheckBox("Continuous checking") {
- tooltip = "Continuous checking of proof document (visible and required parts)"
- reactions += { case ButtonClicked(_) => continuous_checking.update(selected) }
- def load(): Unit = { selected = continuous_checking() }
- load()
- }
- }
-
- 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.Bool_Access("editor_output_state") {
- override def changed(): Unit = GUI_Thread.require {
- super.changed()
- PIDE.editor.flush_edits(hidden = true)
- PIDE.editor.flush()
- }
-
- class GUI extends CheckBox("Proof state") {
- tooltip = "Output of proof state (normally shown on State panel)"
- reactions += { case ButtonClicked(_) => output_state.update(selected) }
- def load(): Unit = { selected = output_state() }
- load()
- }
- }
+ def set_continuous_checking(): Unit = JEdit_Options.continuous_checking.set()
+ def reset_continuous_checking(): Unit = JEdit_Options.continuous_checking.reset()
+ def toggle_continuous_checking(): Unit = JEdit_Options.continuous_checking.toggle()
/* update state */
--- a/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 18:06:30 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 21:23:59 2022 +0200
@@ -26,8 +26,13 @@
}
object JEdit_Options {
+ /* sections */
+
val RENDERING_SECTION = "Rendering of Document Content"
+
+ /* typed access */
+
class Access[A](access: Options.Access_Variable[A], val name: String) {
def apply(): A = access.apply(name)
def update(x: A): Unit = change(_ => x)
@@ -45,6 +50,38 @@
def reset(): Unit = update(false)
def toggle(): Unit = change(b => !b)
}
+
+
+ /* specific options */
+
+ object continuous_checking extends Bool_Access("editor_continuous_checking") {
+ override def changed(): Unit = {
+ super.changed()
+ PIDE.plugin.deps_changed()
+ }
+
+ class GUI extends CheckBox("Continuous checking") {
+ tooltip = "Continuous checking of proof document (visible and required parts)"
+ reactions += { case ButtonClicked(_) => continuous_checking.update(selected) }
+ def load(): Unit = { selected = continuous_checking() }
+ load()
+ }
+ }
+
+ object output_state extends Bool_Access("editor_output_state") {
+ override def changed(): Unit = GUI_Thread.require {
+ super.changed()
+ PIDE.editor.flush_edits(hidden = true)
+ PIDE.editor.flush()
+ }
+
+ class GUI extends CheckBox("Proof state") {
+ tooltip = "Output of proof state (normally shown on State panel)"
+ reactions += { case ButtonClicked(_) => output_state.update(selected) }
+ def load(): Unit = { selected = output_state() }
+ load()
+ }
+ }
}
class JEdit_Options(init_options: Options) extends Options_Variable(init_options) {
--- a/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 18:06:30 2022 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 21:23:59 2022 +0200
@@ -109,7 +109,7 @@
private def delay_load_activated(): Boolean =
delay_load_active.guarded_access(a => Some((!a, true)))
private def delay_load_action(): Unit = {
- if (Isabelle.continuous_checking() && delay_load_activated() &&
+ if (JEdit_Options.continuous_checking() && delay_load_activated() &&
PerspectiveManager.isPerspectiveEnabled) {
if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
else {
@@ -189,7 +189,7 @@
case Session.Ready if !shutting_down.value =>
init_models()
- if (!Isabelle.continuous_checking()) {
+ if (!JEdit_Options.continuous_checking()) {
GUI_Thread.later {
val answer =
GUI.confirm_dialog(jEdit.getActiveView,
@@ -198,7 +198,7 @@
"Continuous checking is presently disabled:",
"editor buffers will remain inactive!",
"Enable continuous checking now?")
- if (answer == 0) Isabelle.continuous_checking.set()
+ if (answer == 0) JEdit_Options.continuous_checking.set()
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 18:06:30 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 21:23:59 2022 +0200
@@ -51,7 +51,7 @@
val new_output =
if (restriction.isEmpty || restriction.get.contains(command))
- Rendering.output_messages(results, Isabelle.output_state())
+ Rendering.output_messages(results, JEdit_Options.output_state())
else current_output
if (current_output != new_output) {
@@ -64,7 +64,7 @@
/* controls */
- private val output_state_button = new Isabelle.output_state.GUI
+ private val output_state_button = new JEdit_Options.output_state.GUI
private val auto_update_button = new CheckBox("Auto update") {
tooltip = "Indicate automatic update following cursor movement"
--- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 18:06:30 2022 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 21:23:59 2022 +0200
@@ -80,7 +80,7 @@
reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
}
- private val continuous_checking = new Isabelle.continuous_checking.GUI
+ private val continuous_checking = new JEdit_Options.continuous_checking.GUI
continuous_checking.focusable = false
private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true)