updated option names;

jedit_linter/etc/options

@@ -1,10 +1,10 @@
 section "Linter"
 
-public option linter : bool = true
+public option linter_enabled : bool = true
   -- "enable linter"
 
 public option lint_all : bool = true
   -- "display the lints of the whole document"
 
-public option show_descriptions : bool = true
+public option lint_descriptions : bool = true
   -- "display the descriptions of the lints"

jedit_linter/src/linter_dockable.scala

@@ -92,12 +92,12 @@ class Linter_Dockable(view: View, position: String) extends Dockable(view, posit
 
   /* controls */
 
-  private def lint_all: Boolean = PIDE.options.bool("lint_all")
+  private def lint_all: Boolean = PIDE.options.bool(LINT_ALL)
 
   private def lint_all_=(b: Boolean): Unit =
   {
     if (lint_all != b) {
-      PIDE.options.bool("lint_all") = b
+      PIDE.options.bool(LINT_ALL) = b
       PIDE.editor.flush_edits(hidden = true)
       PIDE.editor.flush()
     }
@@ -111,12 +111,12 @@ class Linter_Dockable(view: View, position: String) extends Dockable(view, posit
     selected = lint_all
   }
 
-  private def show_descriptions: Boolean = PIDE.options.bool("show_descriptions")
+  private def show_descriptions: Boolean = PIDE.options.bool("lint_descriptions")
 
   private def show_descriptions_=(b: Boolean): Unit =
   {
     if (show_descriptions != b) {
-      PIDE.options.bool("show_descriptions") = b
+      PIDE.options.bool(LINT_DESCRIPTIONS) = b
       PIDE.editor.flush_edits(hidden = true)
       PIDE.editor.flush()
     }
@@ -139,12 +139,12 @@ class Linter_Dockable(view: View, position: String) extends Dockable(view, posit
     reactions += { case ButtonClicked(_) => handle_lint() }
   }
 
-  private def linter: Boolean = PIDE.options.bool("linter")
+  private def linter: Boolean = PIDE.options.bool("linter_enabled")
 
   private def linter_=(b: Boolean): Unit =
   {
     if (linter != b) {
-      PIDE.options.bool("linter") = b
+      PIDE.options.bool("linter_enabled") = b
       Linter_Plugin.instance.foreach { plugin =>
         plugin.linter.update(PIDE.options.value)
         plugin.overlays.clear()

jedit_linter/src/linter_variable.scala

@@ -13,8 +13,6 @@ import isabelle.linter._
 
 class Linter_Variable
 {
-  val LINTER_ENABLED_OPTION = "linter"
-
   private var lint_cache: Map[Document.Node.Name, (Document.Version, Linter.Lint_Report)] = Map.empty
   private var lint_selection: Lint_Store.Selection = Lint_Store.Selection.empty
   private var _enabled: Boolean = false
@@ -32,7 +30,7 @@ class Linter_Variable
   def enabled: Boolean = _enabled
 
   def update(options: Options): Unit = synchronized {
-    this._enabled = options.bool(LINTER_ENABLED_OPTION)
+    this._enabled = options.bool("linter_enabled")
     if (_enabled) this.lint_selection = Lint_Store.Selection(options)
   }
 

linter_base/etc/options

@@ -1,10 +1,10 @@
 section "Linter"
 
-public option enabled_bundles : string = "default"
+public option lint_bundles : string = "default"
   -- "enabled lint bundles"
 
-public option enabled_lints : string = ""
+public option lints_enabled : string = ""
   -- "extra enabled lints"
 
-public option disabled_lints : string = ""
+public option lints_disabled : string = ""
   -- "disabled lints"

linter_base/src/lint_store.scala

@@ -203,15 +203,11 @@ print the lints belonging to each bundle.
 
   object Selection
   {
-    val ENABLED_BUNDLES_OPTION = "enabled_bundles"
-    val ENABLED_LINTS_OPTION = "enabled_lints"
-    val DISABLED_LINTS_OPTION = "disabled_lints"
-
     def apply(options: Options): Selection =
     {
-      val bundles = space_explode(',', options.string(ENABLED_BUNDLES_OPTION))
-      val enabled_lints = space_explode(',', options.string(ENABLED_LINTS_OPTION))
-      val disabled_lints = space_explode(',', options.string(DISABLED_LINTS_OPTION))
+      val bundles = space_explode(',', options.string("lint_bundles"))
+      val enabled_lints = space_explode(',', options.string("lints_enabled"))
+      val disabled_lints = space_explode(',', options.string("lints_disabled"))
 
       Selection.empty
         .add_bundles(bundles)