# HG changeset patch
# User wenzelm
# Date 1364403861 -3600
# Node ID 91f8bed6d0a4a50c5e0fd778f107d8a83bc99cb5
# Parent  4e4b56b7a3a531ab463d0c2260b13242f380e5de
allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;

diff -r 4e4b56b7a3a5 -r 91f8bed6d0a4 src/Doc/ROOT
--- a/src/Doc/ROOT	Wed Mar 27 17:58:07 2013 +0100
+++ b/src/Doc/ROOT	Wed Mar 27 18:04:21 2013 +0100
@@ -40,7 +40,7 @@
     "document/style.sty"
 
 session Functions (doc) in "Functions" = HOL +
-  options [document_variants = "functions"]
+  options [document_variants = "functions", skip_proofs = false]
   theories Functions
   files
     "../prepare_document"
@@ -145,7 +145,7 @@
     "document/root.tex"
 
 session Locales (doc) in "Locales" = HOL +
-  options [document_variants = "locales", pretty_margin = 65]
+  options [document_variants = "locales", pretty_margin = 65, skip_proofs = false]
   theories
     Examples1
     Examples2
@@ -295,7 +295,7 @@
     "document/root.tex"
 
 session Tutorial (doc) in "Tutorial" = HOL +
-  options [document_variants = "tutorial", print_mode = "brackets"]
+  options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
   theories [thy_output_indent = 5]
     "ToyList/ToyList"
     "Ifexpr/Ifexpr"
diff -r 4e4b56b7a3a5 -r 91f8bed6d0a4 src/FOL/ROOT
--- a/src/FOL/ROOT	Wed Mar 27 17:58:07 2013 +0100
+++ b/src/FOL/ROOT	Wed Mar 27 18:04:21 2013 +0100
@@ -39,6 +39,7 @@
     Quantifiers_Cla
     Miniscope
     If
-  theories [document = false] "Locale_Test/Locale_Test"
+  theories [document = false, skip_proofs = false]
+    "Locale_Test/Locale_Test"
   files "document/root.tex"
 
diff -r 4e4b56b7a3a5 -r 91f8bed6d0a4 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Mar 27 17:58:07 2013 +0100
+++ b/src/HOL/ROOT	Wed Mar 27 18:04:21 2013 +0100
@@ -16,7 +16,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, proofs = 2]
+  options [document = false, proofs = 2, skip_proofs = false]
   theories Main
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
@@ -354,14 +354,14 @@
   theories Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
-  options [document = false, proofs = 2, parallel_proofs = 0]
+  options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
   theories Hilbert_Classical
 
 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
+  options [condition = ISABELLE_POLYML, proofs = 2, skip_proofs = false, parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -386,7 +386,8 @@
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
-  options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
+  options [document_graph, print_mode = "no_brackets", proofs = 2, skip_proofs = false,
+    parallel_proofs = 0]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
   theories
@@ -535,7 +536,6 @@
     Tarski
     Classical
     Set_Theory
-    Meson_Test
     Termination
     Coherent
     PresburgerEx
@@ -561,6 +561,8 @@
     Parallel_Example
     IArray_Examples
   theories SVC_Oracle
+  theories [skip_proofs = false]
+    Meson_Test
   theories [condition = SVC_HOME]
     svc_test
   theories [condition = ZCHAFF_HOME]
@@ -742,7 +744,8 @@
   theories WordExamples
 
 session "HOL-Statespace" in Statespace = HOL +
-  theories StateSpaceEx
+  theories [skip_proofs = false]
+    StateSpaceEx
   files "document/root.tex"
 
 session "HOL-NSA" in NSA = HOL +