clarified signature: more explicit types;

--- 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))

--- 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)

--- 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()
+    }
   }
 
 

--- 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) {

--- 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()
         }
       }
 

--- 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)
         }
 

--- 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)