avoid accidental update of base session sources (following documentation in "system" manual);
authorwenzelm
Fri, 20 Mar 2020 19:55:42 +0100
changeset 71573 c67076c07fb8
parent 71572 f55222fbeae3
child 71574 95460356d633
avoid accidental update of base session sources (following documentation in "system" manual);
src/Pure/Tools/dump.scala
src/Pure/Tools/update.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 =
--- 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)