clarified vacuous selection vs. Pure;
authorwenzelm
Sun, 24 Nov 2019 15:45:32 +0100
changeset 71357 6b03ce9b02c7
parent 71356 1c58a01a372e
child 71358 625df1eb7873
clarified vacuous selection vs. Pure;
src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sun Nov 24 15:31:28 2019 +0100
+++ b/src/Pure/Tools/dump.scala	Sun Nov 24 15:45:32 2019 +0100
@@ -171,15 +171,17 @@
       def make_session(
         selected_sessions: List[String],
         session_logic: String = logic,
+        strict: Boolean = false,
         record_proofs: Boolean = false): List[Session] =
       {
-        if (selected_sessions.isEmpty) Nil
+        if (selected_sessions.isEmpty && !strict) Nil
         else List(new Session(context, session_logic, log, selected_sessions, record_proofs))
       }
 
       val base =
-        if (logic == isabelle.Thy_Header.PURE) Nil
-        else make_session(base_sessions, session_logic = isabelle.Thy_Header.PURE)
+        make_session(base_sessions,
+          session_logic = isabelle.Thy_Header.PURE,
+          strict = logic == isabelle.Thy_Header.PURE)
 
       val main =
         make_session(