--- a/src/Doc/System/Sessions.thy Thu Jan 05 22:16:13 2023 +0100
+++ b/src/Doc/System/Sessions.thy Thu Jan 05 22:30:20 2023 +0100
@@ -784,10 +784,10 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
- -b NAME additional base logic
-d DIR include session directory
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
+ -l NAME additional base logic
-n no build -- take existing build databases
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u OPT override "update" option: shortcut for "-o update_OPT"
@@ -805,7 +805,7 @@
\<^medskip> Option \<^verbatim>\<open>-n\<close> suppresses the actual build process, but existing build
databases are used nonetheless.
- \<^medskip> Option \<^verbatim>\<open>-b\<close> specifies one or more base logics: these sessions and their
+ \<^medskip> Option \<^verbatim>\<open>-l\<close> specifies one or more base logics: these sessions and their
ancestors are \<^emph>\<open>excluded\<close> from the update.
\<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
@@ -859,7 +859,7 @@
\<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close>, but
do not change the underlying \<^verbatim>\<open>HOL\<close> (and \<^verbatim>\<open>Pure\<close>) session:
- @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -b HOL -B HOL-Analysis\<close>}
+ @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -l HOL -B HOL-Analysis\<close>}
\<^smallskip> Update all sessions that happen to be properly built beforehand:
--- a/src/Pure/Tools/update.scala Thu Jan 05 22:16:13 2023 +0100
+++ b/src/Pure/Tools/update.scala Thu Jan 05 22:30:20 2023 +0100
@@ -119,8 +119,8 @@
var all_sessions = false
var dirs: List[Path] = Nil
var session_groups: List[String] = Nil
+ var max_jobs = 1
var base_logics: List[String] = Nil
- var max_jobs = 1
var no_build = false
var options = Options.init()
var verbose = false
@@ -135,10 +135,10 @@
-R refer to requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
- -b NAME additional base logic
-d DIR include session directory
-g NAME select session group NAME
-j INT maximum number of parallel jobs (default 1)
+ -l NAME additional base logic
-n no build -- take existing build databases
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-u OPT override "update" option: shortcut for "-o update_OPT"
@@ -153,10 +153,10 @@
"R" -> (_ => requirements = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
- "b:" -> (arg => base_logics ::= arg),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"g:" -> (arg => session_groups = session_groups ::: List(arg)),
"j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+ "l:" -> (arg => base_logics ::= arg),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
"u:" -> (arg => options = options + ("update_" + arg)),