clarified syntax;
authorwenzelm
Tue Jun 26 19:03:13 2018 +0200 (13 months ago)
changeset 6851216ae55c77bcb
parent 68511 c6626358bf21
child 68513 88b0e63d58a5
clarified syntax;
src/HOL/ROOT
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/HOL/ROOT	Tue Jun 26 18:44:51 2018 +0200
     1.2 +++ b/src/HOL/ROOT	Tue Jun 26 19:03:13 2018 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4    document_files "root.bib" "root.tex"
     1.5  
     1.6  session "HOL-Analysis" (main timing) in Analysis = HOL +
     1.7 -  options [document_tags = "*=unimportant",
     1.8 +  options [document_tags = "%unimportant",
     1.9      document_variants = "document:manual=-proof,-ML,-unimportant"]
    1.10    sessions
    1.11      "HOL-Library"
     2.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 18:44:51 2018 +0200
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 19:03:13 2018 +0200
     2.3 @@ -240,8 +240,8 @@
     2.4  fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
     2.5  
     2.6  fun read_tag s =
     2.7 -  (case space_explode "=" s of
     2.8 -    ["*", b] => (SOME b, NONE)
     2.9 +  (case space_explode "%" s of
    2.10 +    ["", b] => (SOME b, NONE)
    2.11    | [a, b] => (NONE, SOME (a, b))
    2.12    | _ => error ("Bad document_tags specification: " ^ quote s));
    2.13