# HG changeset patch
# User wenzelm
# Date 1574606732 -3600
# Node ID 6b03ce9b02c75b56a1946805e1cf3380cb10e8f7
# Parent  1c58a01a372e35e131aa9bfec446d21338c53cb4
clarified vacuous selection vs. Pure;

diff -r 1c58a01a372e -r 6b03ce9b02c7 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(