# HG changeset patch
# User wenzelm
# Date 1584730542 -3600
# Node ID c67076c07fb82fb3ff712d7131e1a3026ef47721
# Parent  f55222fbeae35cc703d770344df4ea0b5cb7eb86
avoid accidental update of base session sources (following documentation in "system" manual);

diff -r f55222fbeae3 -r c67076c07fb8 src/Pure/Tools/dump.scala
--- 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 =
diff -r f55222fbeae3 -r c67076c07fb8 src/Pure/Tools/update.scala
--- 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)