# HG changeset patch
# User wenzelm
# Date 1678542593 -3600
# Node ID 29effd67d8a88830bdd2c140637491b3bb6cadb7
# Parent  faaa3e311281bd5df1bdc4a662025ace62d921b8
support "isabelle options -l -t TAGS";

diff -r faaa3e311281 -r 29effd67d8a8 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Mar 11 14:19:09 2023 +0100
+++ b/src/Doc/System/Sessions.thy	Sat Mar 11 14:49:53 2023 +0100
@@ -326,7 +326,8 @@
     -b           include $ISABELLE_BUILD_OPTIONS
     -g OPTION    get value of OPTION
     -l           list options
-    -x FILE      export to FILE in YXML format
+    -t TAGS      restrict list to given tags (comma-separated)
+    -x FILE      export options to FILE in YXML format
 
   Report Isabelle system options, augmented by MORE_OPTIONS given as
   arguments NAME=VAL or NAME.\<close>}
@@ -338,7 +339,8 @@
   of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
 
   Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
-  options with their declaration and current value.
+  options with their declaration and current value. Option \<^verbatim>\<open>-t\<close> restricts the
+  listing to given tags (as comma-separated list), e.g. \<^verbatim>\<open>-t build,document\<close>.
 
   Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
   of printing it in human-readable form.
diff -r faaa3e311281 -r 29effd67d8a8 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Sat Mar 11 14:19:09 2023 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 11 14:49:53 2023 +0100
@@ -194,6 +194,7 @@
       var build_options = false
       var get_option = ""
       var list_options = false
+      var list_tags = List.empty[String]
       var export_file = ""
 
       val getopts = Getopts("""
@@ -203,6 +204,7 @@
     -b           include $ISABELLE_BUILD_OPTIONS
     -g OPTION    get value of OPTION
     -l           list options
+    -t TAGS      restrict list to given tags (comma-separated)
     -x FILE      export options to FILE in YXML format
 
   Report Isabelle system options, augmented by MORE_OPTIONS given as
@@ -211,6 +213,7 @@
         "b" -> (_ => build_options = true),
         "g:" -> (arg => get_option = arg),
         "l" -> (_ => list_options = true),
+        "t:" -> (arg => list_tags = space_explode(',', arg)),
         "x:" -> (arg => export_file = arg))
 
       val more_options = getopts(args)
@@ -235,7 +238,10 @@
       }
 
       if (get_option == "" && export_file == "") {
-        Output.writeln(options.print, stdout = true)
+        val filter: Options.Entry => Boolean =
+          if (list_tags.isEmpty) (_ => true)
+          else opt => list_tags.exists(opt.has_tag)
+        Output.writeln(options.print(filter = filter), stdout = true)
       }
     })
 }
@@ -252,7 +258,8 @@
   private def print_entry(opt: Options.Entry): String =
     if_proper(opt.public, "public ") + opt.print
 
-  def print: String = cat_lines(iterator.toList.sortBy(_.name).map(print_entry))
+  def print(filter: Options.Entry => Boolean = _ => true): String =
+    cat_lines(iterator.filter(filter).toList.sortBy(_.name).map(print_entry))
 
   def description(name: String): String = check_name(name).description