# HG changeset patch # User wenzelm # Date 1660403925 -7200 # Node ID 93436389db1cd315e69c50a7cf45d06d0ea22d86 # Parent d9926523855e7a7dcd04b0da28031b778caf3297 clarified signature: more explicit types; diff -r d9926523855e -r 93436389db1c src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Pure/System/options.scala Sat Aug 13 17:18:45 2022 +0200 @@ -13,16 +13,22 @@ val empty: Options = new Options() - /* access */ + /* typed access */ abstract class Access[A](val options: Options) { def apply(name: String): A def update(name: String, x: A): Options + def change(name: String, f: A => A): Options = update(name, f(apply(name))) } - abstract class Access_Variable[A](val options: Options_Variable) { - def apply(name: String): A - def update(name: String, x: A): Unit + class Access_Variable[A]( + val options: Options_Variable, + val pure_access: Options => Access[A] + ) { + def apply(name: String): A = pure_access(options.value)(name) + def update(name: String, x: A): Unit = + options.change(options => pure_access(options).update(name, x)) + def change(name: String, f: A => A): Unit = update(name, f(apply(name))) } @@ -428,28 +434,16 @@ def += (name: String, x: String): Unit = change(options => options + (name, x)) val bool: Options.Access_Variable[Boolean] = - new Options.Access_Variable[Boolean](this) { - def apply(name: String): Boolean = value.bool(name) - def update(name: String, x: Boolean): Unit = change(options => options.bool.update(name, x)) - } + new Options.Access_Variable[Boolean](this, _.bool) val int: Options.Access_Variable[Int] = - new Options.Access_Variable[Int](this) { - def apply(name: String): Int = value.int(name) - def update(name: String, x: Int): Unit = change(options => options.int.update(name, x)) - } + new Options.Access_Variable[Int](this, _.int) val real: Options.Access_Variable[Double] = - new Options.Access_Variable[Double](this) { - def apply(name: String): Double = value.real(name) - def update(name: String, x: Double): Unit = change(options => options.real.update(name, x)) - } + new Options.Access_Variable[Double](this, _.real) val string: Options.Access_Variable[String] = - new Options.Access_Variable[String](this) { - def apply(name: String): String = value.string(name) - def update(name: String, x: String): Unit = change(options => options.string.update(name, x)) - } + new Options.Access_Variable[String](this, _.string) def proper_string(name: String): Option[String] = Library.proper_string(string(name)) diff -r d9926523855e -r 93436389db1c src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Aug 13 17:18:45 2022 +0200 @@ -342,7 +342,7 @@ ): (Boolean, Document.Node.Perspective_Text) = { GUI_Thread.require {} - if (Isabelle.continuous_checking && is_theory) { + if (Isabelle.continuous_checking() && is_theory) { val snapshot = this.snapshot() val reparse = snapshot.node.load_commands_changed(doc_blobs) diff -r d9926523855e -r 93436389db1c src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Sat Aug 13 17:18:45 2022 +0200 @@ -195,27 +195,42 @@ /* continuous checking */ - private val CONTINUOUS_CHECKING = "editor_continuous_checking" - - def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING) - def continuous_checking_=(b: Boolean): Unit = - GUI_Thread.require { - if (continuous_checking != b) { - PIDE.options.bool(CONTINUOUS_CHECKING) = b - PIDE.session.update_options(PIDE.options.value) - PIDE.plugin.deps_changed() - } + object continuous_checking + extends JEdit_Options.Access(PIDE.options.bool, "editor_continuous_checking") { + override def changed(): Unit = { + super.changed() + PIDE.plugin.deps_changed() } - def set_continuous_checking(): Unit = { continuous_checking = true } - def reset_continuous_checking(): Unit = { continuous_checking = false } - def toggle_continuous_checking(): Unit = { continuous_checking = !continuous_checking } + 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.update(true) + def reset_continuous_checking(): Unit = continuous_checking.update(false) + def toggle_continuous_checking(): Unit = continuous_checking.change(b => !b) + + + /* output state */ - class Continuous_Checking extends CheckBox("Continuous checking") { - tooltip = "Continuous checking of proof document (visible and required parts)" - reactions += { case ButtonClicked(_) => continuous_checking = selected } - def load(): Unit = { selected = continuous_checking } - load() + object output_state + extends JEdit_Options.Access(PIDE.options.bool, "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() + } } diff -r d9926523855e -r 93436389db1c src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Sat Aug 13 17:18:45 2022 +0200 @@ -27,6 +27,18 @@ object JEdit_Options { val RENDERING_SECTION = "Rendering of Document Content" + + class Access[A](access: Options.Access_Variable[A], val name: String) { + def apply(): A = access.apply(name) + def update(x: A): Unit = change(_ => x) + def change(f: A => A): Unit = { + val x0 = apply() + access.change(name, f) + val x1 = apply() + if (x0 != x1) changed() + } + def changed(): Unit = GUI_Thread.require { PIDE.session.update_options(access.options.value) } + } } class JEdit_Options(init_options: Options) extends Options_Variable(init_options) { diff -r d9926523855e -r 93436389db1c src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Tools/jEdit/src/main_plugin.scala Sat Aug 13 17:18:45 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 (Isabelle.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 (!Isabelle.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 = true + if (answer == 0) Isabelle.set_continuous_checking() } } diff -r d9926523855e -r 93436389db1c src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 17:18:45 2022 +0200 @@ -51,7 +51,7 @@ val new_output = if (restriction.isEmpty || restriction.get.contains(command)) - Rendering.output_messages(results, output_state) + Rendering.output_messages(results, Isabelle.output_state()) else current_output if (current_output != new_output) { @@ -64,21 +64,7 @@ /* controls */ - private def output_state: Boolean = PIDE.options.bool("editor_output_state") - private def output_state_=(b: Boolean): Unit = { - if (output_state != b) { - PIDE.options.bool("editor_output_state") = b - PIDE.session.update_options(PIDE.options.value) - PIDE.editor.flush_edits(hidden = true) - PIDE.editor.flush() - } - } - - private val output_state_button = new CheckBox("Proof state") { - tooltip = "Output of proof state (normally shown on State panel)" - reactions += { case ButtonClicked(_) => output_state = selected } - selected = output_state - } + private val output_state_button = new Isabelle.output_state.GUI private val auto_update_button = new CheckBox("Auto update") { tooltip = "Indicate automatic update following cursor movement" @@ -110,7 +96,7 @@ case _: Session.Global_Options => GUI_Thread.later { handle_resize() - output_state_button.selected = output_state + output_state_button.load() handle_update(do_update, None) } diff -r d9926523855e -r 93436389db1c src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 16:24:14 2022 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Sat Aug 13 17:18:45 2022 +0200 @@ -80,7 +80,7 @@ reactions += { case ButtonClicked(_) => PIDE.editor.purge() } } - private val continuous_checking = new Isabelle.Continuous_Checking + private val continuous_checking = new Isabelle.continuous_checking.GUI continuous_checking.focusable = false private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true)