# HG changeset patch
# User wenzelm
# Date 1660418639 -7200
# Node ID dfedac6525d4aa0e0e01807be0a37d70cff27212
# Parent  9e4c0aaa30aa5553e39a2ea7910dc27413de17d2
clarified modules;

diff -r 9e4c0aaa30aa -r dfedac6525d4 src/Tools/jEdit/src/document_model.scala
--- 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)
diff -r 9e4c0aaa30aa -r dfedac6525d4 src/Tools/jEdit/src/isabelle.scala
--- 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 */
diff -r 9e4c0aaa30aa -r dfedac6525d4 src/Tools/jEdit/src/jedit_options.scala
--- 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) {
diff -r 9e4c0aaa30aa -r dfedac6525d4 src/Tools/jEdit/src/main_plugin.scala
--- 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()
         }
       }
 
diff -r 9e4c0aaa30aa -r dfedac6525d4 src/Tools/jEdit/src/output_dockable.scala
--- 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"
diff -r 9e4c0aaa30aa -r dfedac6525d4 src/Tools/jEdit/src/theories_dockable.scala
--- 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)