Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified syntax;
authorwenzelm
Tue, 26 Jun 2018 19:03:13 +0200
changeset 68512 16ae55c77bcb
parent 68511 c6626358bf21
child 68513 88b0e63d58a5
clarified syntax;
src/HOL/ROOT file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_output.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/ROOT	Tue Jun 26 18:44:51 2018 +0200
+++ b/src/HOL/ROOT	Tue Jun 26 19:03:13 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"
--- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 18:44:51 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 19:03:13 2018 +0200
@@ -240,8 +240,8 @@
 fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
 
 fun read_tag s =
-  (case space_explode "=" s of
-    ["*", b] => (SOME b, NONE)
+  (case space_explode "%" s of
+    ["", b] => (SOME b, NONE)
   | [a, b] => (NONE, SOME (a, b))
   | _ => error ("Bad document_tags specification: " ^ quote s));
isabelle