# HG changeset patch
# User wenzelm
# Date 1530027769 -7200
# Node ID 795f39bfe4e15029eca0810da434917a7399e53b
# Parent  0f91ff642658ca2a241862f20d9ca3e6d9d64b6e
simplified: allow only command names, with dummy for default;

diff -r 0f91ff642658 -r 795f39bfe4e1 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jun 26 17:25:57 2018 +0200
+++ b/src/HOL/ROOT	Tue Jun 26 17:42:49 2018 +0200
@@ -58,7 +58,7 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
-  options [document_tags = "unimportant",
+  options [document_tags = "*=unimportant",
     document_variants = "document:manual=-proof,-ML,-unimportant"]
   sessions
     "HOL-Library"
diff -r 0f91ff642658 -r 795f39bfe4e1 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 17:25:57 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 17:42:49 2018 +0200
@@ -241,12 +241,8 @@
 
 fun read_tag s =
   (case space_explode "=" s of
-    [] => (SOME s, NONE, NONE)
-  | [_] => (SOME s, NONE, NONE)
-  | [a, b] =>
-      if String.isPrefix "[" a andalso String.isSuffix "]" a
-      then (NONE, SOME (unenclose a, b), NONE)
-      else (NONE, NONE, SOME (a, b))
+    ["*", b] => (SOME b, NONE)
+  | [a, b] => (NONE, SOME (a, b))
   | _ => error ("Bad document_tags specification: " ^ quote s));
 
 in
@@ -256,8 +252,7 @@
     val document_tags =
       map read_tag (space_explode "," (Options.string options \<^system_option>\<open>document_tags\<close>));
     val document_tags_default = map_filter #1 document_tags;
-    val document_tags_category = map_filter #2 document_tags;
-    val document_tags_command = map_filter #3 document_tags;
+    val document_tags_command = map_filter #2 document_tags;
   in
     fn {cmd_name, cmd_tags, tag, active_tag} => fn state => fn state' =>
       let
@@ -268,7 +263,6 @@
           else Keyword.command_tags keywords cmd_name;
         val command_tags =
           the_list (AList.lookup (op =) document_tags_command cmd_name) @
-          map_filter (AList.lookup (op =) document_tags_category) keyword_tags @
           keyword_tags @ document_tags_default;
 
         val active_tag' =