avoid accidental update of base session sources (following documentation in "system" manual);
--- a/src/Pure/Tools/dump.scala Fri Mar 20 16:21:58 2020 +0100
+++ b/src/Pure/Tools/dump.scala Fri Mar 20 19:55:42 2020 +0100
@@ -98,7 +98,8 @@
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty,
- pure_base: Boolean = false): Context =
+ pure_base: Boolean = false,
+ skip_base: Boolean = false): Context =
{
val session_options: Options =
{
@@ -125,7 +126,7 @@
val deps: Sessions.Deps =
Sessions.deps(sessions_structure, progress = progress).check_errors
- new Context(options, progress, dirs, select_dirs, pure_base, session_options, deps)
+ new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps)
}
}
@@ -135,6 +136,7 @@
val dirs: List[Path],
val select_dirs: List[Path],
val pure_base: Boolean,
+ val skip_base: Boolean,
val session_options: Options,
val deps: Sessions.Deps)
{
@@ -189,7 +191,7 @@
val PURE = isabelle.Thy_Header.PURE
val base =
- if (logic == PURE && !pure_base) Nil
+ if ((logic == PURE && !pure_base) || skip_base) Nil
else make_session(base_sessions, session_logic = PURE, strict = logic == PURE)
val main =
--- a/src/Pure/Tools/update.scala Fri Mar 20 16:21:58 2020 +0100
+++ b/src/Pure/Tools/update.scala Fri Mar 20 19:55:42 2020 +0100
@@ -18,7 +18,7 @@
{
val context =
Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
- selection = selection)
+ selection = selection, skip_base = true)
context.build_logic(logic)