# HG changeset patch
# User wenzelm
# Date 1678547486 -3600
# Node ID 58b7f3fb73cbd3aece584bf8955434a3e0b75bcb
# Parent  29effd67d8a88830bdd2c140637491b3bb6cadb7
tuned signature;

diff -r 29effd67d8a8 -r 58b7f3fb73cb src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Mar 11 14:49:53 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 16:11:26 2023 +0100
@@ -91,9 +91,12 @@
 
     def unknown: Boolean = typ == Unknown
 
-    def has_tag(tag: String): Boolean = tags.contains(tag)
-    def session_content: Boolean = has_tag(TAG_CONTENT) || has_tag(TAG_DOCUMENT)
-    def color_dialog: Boolean = has_tag(TAG_COLOR_DIALOG)
+    def for_tag(tag: String): Boolean = tags.contains(tag)
+    def for_content: Boolean = for_tag(TAG_CONTENT)
+    def for_document: Boolean = for_tag(TAG_DOCUMENT)
+    def for_color_dialog: Boolean = for_tag(TAG_COLOR_DIALOG)
+
+    def session_content: Boolean = for_content || for_document
   }
 
 
@@ -240,7 +243,7 @@
       if (get_option == "" && export_file == "") {
         val filter: Options.Entry => Boolean =
           if (list_tags.isEmpty) (_ => true)
-          else opt => list_tags.exists(opt.has_tag)
+          else opt => list_tags.exists(opt.for_tag)
         Output.writeln(options.print(filter = filter), stdout = true)
       }
     })
@@ -453,9 +456,6 @@
       .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
   }
 
-  def session_prefs(defaults: Options = Options.init0()): String =
-    make_prefs(defaults = defaults, filter = _.session_content)
-
   def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init0()): Unit = {
     val prefs = make_prefs(defaults = defaults)
     Isabelle_System.make_directory(file.dir)
diff -r 29effd67d8a8 -r 58b7f3fb73cb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Mar 11 14:49:53 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Mar 11 16:11:26 2023 +0100
@@ -629,7 +629,7 @@
 
         val entry_options = entry.options ::: augment_options(name)
         val session_options = options ++ entry_options
-        val session_prefs = options.session_prefs(defaults = options0)
+        val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
 
         val theories =
           entry.theories.map({ case (opts, thys) =>
@@ -825,7 +825,7 @@
         }
 
       val options0 = Options.init0()
-      val session_prefs = options.session_prefs(defaults = options0)
+      val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
 
       val root_infos = {
         var chapter = UNSORTED
diff -r 29effd67d8a8 -r 58b7f3fb73cb src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Sat Mar 11 14:49:53 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat Mar 11 16:11:26 2023 +0100
@@ -122,7 +122,7 @@
     private val predefined =
       (for {
         opt <- PIDE.options.value.iterator
-        if opt.color_dialog
+        if opt.for_color_dialog
       } yield PIDE.options.make_color_component(opt)).toList
 
     assert(predefined.nonEmpty)