clarified vacuous selection vs. Pure;

--- 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(