# HG changeset patch
# User wenzelm
# Date 1537541223 -7200
# Node ID 6e2f9f62aafdaa2a6dc5e23afc06539ab7d570b4
# Parent  fa7a1be0fab2d0e195099643e1db0b1c5b9efc64
suppress some theories to allow "isabelle dump -o skip_proofs";

diff -r fa7a1be0fab2 -r 6e2f9f62aafd src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 21 14:31:07 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 21 16:47:03 2018 +0200
@@ -196,21 +196,28 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def used_theories_condition(warning: String => Unit = _ => ())
+    def used_theories_condition(default_options: Options, warning: String => Unit = _ => ())
       : List[(Options, Document.Node.Name)] =
     {
+      val default_skip_proofs = default_options.bool("skip_proofs")
       for {
         session_name <- sessions_structure.build_topological_order
         (options, name) <- session_bases(session_name).used_theories
         if {
+          def warn(msg: String): Unit = warning("Skipping theory " + name + "  (" + msg + ")")
+
           val conditions =
             space_explode(',', options.string("condition")).
               filter(cond => Isabelle_System.getenv(cond) == "")
-          if (conditions.isEmpty) true
-          else {
-            warning("Skipping theory " + name + "  (condition " + conditions.mkString(" ") + ")")
+          if (conditions.nonEmpty) {
+            warn("condition " + conditions.mkString(" "))
             false
           }
+          else if (default_skip_proofs && !options.bool("skip_proofs")) {
+            warn("option skip_proofs")
+            false
+          }
+          else true
         }
       } yield (options, name)
     }
diff -r fa7a1be0fab2 -r 6e2f9f62aafd src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Sep 21 14:31:07 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Sep 21 16:47:03 2018 +0200
@@ -113,7 +113,7 @@
       deps.sessions_structure.imports_topological_order
 
     val use_theories =
-      for { (_, name) <- deps.used_theories_condition(progress.echo_warning) }
+      for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) }
       yield name.theory