--- a/src/Pure/Tools/dump.scala Sat Nov 23 09:56:11 2019 +0000
+++ b/src/Pure/Tools/dump.scala Sun Nov 24 15:31:28 2019 +0100
@@ -170,19 +170,16 @@
def make_session(
selected_sessions: List[String],
- pure: Boolean = false,
+ session_logic: String = logic,
record_proofs: Boolean = false): List[Session] =
{
if (selected_sessions.isEmpty) Nil
- else {
- val session_logic = if (pure) isabelle.Thy_Header.PURE else logic
- List(new Session(context, session_logic, log, selected_sessions, record_proofs))
- }
+ 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, pure = true)
+ else make_session(base_sessions, session_logic = isabelle.Thy_Header.PURE)
val main =
make_session(
@@ -192,7 +189,7 @@
proof_sessions.contains(name)))
val proofs =
- make_session(proof_sessions, pure = true, record_proofs = true)
+ make_session(proof_sessions, session_logic = isabelle.Thy_Header.PURE, record_proofs = true)
val afp =
if (afp_sessions.isEmpty) Nil