explicit group "no_doc" for unfinished documentation, allows to suppress everything uniformly: -X doc -X no_doc;
authorwenzelm
Tue, 02 Oct 2018 19:20:00 +0200
changeset 69105 b7274dfbf4b3
parent 69104 f33352dbbf12
child 69106 742c88258cf8
explicit group "no_doc" for unfinished documentation, allows to suppress everything uniformly: -X doc -X no_doc;
src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Oct 02 19:10:04 2018 +0200
+++ b/src/Doc/ROOT	Tue Oct 02 19:20:00 2018 +0200
@@ -16,7 +16,7 @@
     "root.tex"
     "style.sty"
 
-session Codegen_Basics in "Codegen" = "HOL-Library" +
+session Codegen_Basics (no_doc) in "Codegen" = "HOL-Library" +
   theories
     Setup
 
@@ -116,7 +116,7 @@
     "root.tex"
     "style.sty"
 
-session How_to_Prove_it (* FIXME (doc) *) in "How_to_Prove_it" = HOL +
+session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL +
   options [document_variants = "how_to_prove_it", show_question_marks = false]
   theories
     How_to_Prove_it
@@ -502,6 +502,6 @@
     "root.tex"
     "style.sty"
 
-session Typeclass_Hierarchy_Basics in "Typeclass_Hierarchy" = "HOL-Library" +
+session Typeclass_Hierarchy_Basics (no_doc) in "Typeclass_Hierarchy" = "HOL-Library" +
   theories
     Setup