# HG changeset patch
# User wenzelm
# Date 1571075918 -7200
# Node ID d1299774543d61f574001ce08691e057396afd94
# Parent  a4ccd277e9c49158748369f1a9639e36ef9fa155
clarified "isabelle update" options -- more like "isabelle dump";

diff -r a4ccd277e9c4 -r d1299774543d src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Mon Oct 14 19:37:12 2019 +0200
+++ b/src/Doc/System/Sessions.thy	Mon Oct 14 19:58:38 2019 +0200
@@ -627,9 +627,9 @@
     -R           operate on requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b NAME      base logic image (default "Pure")
     -d DIR       include session directory
     -g NAME      select session group NAME
-    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -u OPT       overide update option: shortcut for "-o update_OPT"
     -v           verbose
@@ -641,7 +641,9 @@
   remaining command-line arguments specify sessions as in @{tool build}
   (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}).
 
-  \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies the underlying logic image.
+  \<^medskip> Option \<^verbatim>\<open>-b\<close> specifies an optional base logic image, for improved
+  scalability of the PIDE session. Its theories are only processed if it is
+  included in the overall session selection.
 
   \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
 
@@ -687,19 +689,14 @@
 
 text \<open>
   Update some cartouche notation in all theory sources required for session
-  \<^verbatim>\<open>HOL-Analysis\<close>:
+  \<^verbatim>\<open>HOL-Analysis\<close> (and ancestors):
 
-  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l Pure HOL-Analysis\<close>}
+  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches HOL-Analysis\<close>}
 
   \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
-  its image is taken as starting point and its sources are not touched:
-
-  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -l HOL-Analysis -B HOL-Analysis\<close>}
+  using its image is taken starting point (for reduced resource requirements):
 
-  \<^smallskip> This two-stage approach reduces resource requirements of the running PIDE
-  session: a base image like \<^verbatim>\<open>HOL-Analysis\<close> (or \<^verbatim>\<open>HOL\<close>, \<^verbatim>\<open>HOL-Library\<close>) is
-  more compact than importing all required theory (and ML) source files from
-  \<^verbatim>\<open>Pure\<close>.
+  @{verbatim [display] \<open>isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\<close>}
 
   \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
   separately with special options as follows:
diff -r a4ccd277e9c4 -r d1299774543d src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Mon Oct 14 19:37:12 2019 +0200
+++ b/src/Pure/Tools/update.scala	Mon Oct 14 19:58:38 2019 +0200
@@ -68,7 +68,7 @@
       var all_sessions = false
       var dirs: List[Path] = Nil
       var session_groups: List[String] = Nil
-      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+      var logic = Dump.default_logic
       var options = Options.init()
       var verbose = false
       var exclude_sessions: List[String] = Nil
@@ -82,9 +82,9 @@
     -R           operate on requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b NAME      base logic image (default """ + isabelle.quote(Dump.default_logic) + """)
     -d DIR       include session directory
     -g NAME      select session group NAME
-    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -u OPT       overide update option: shortcut for "-o update_OPT"
     -v           verbose
@@ -97,9 +97,9 @@
       "R" -> (_ => requirements = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
+      "b:" -> (arg => logic = arg),
       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
-      "l:" -> (arg => logic = arg),
       "o:" -> (arg => options = options + arg),
       "u:" -> (arg => options = options + ("update_" + arg)),
       "v" -> (_ => verbose = true),