# HG changeset patch
# User wenzelm
# Date 1673003132 -3600
# Node ID d858e6f15da3e6fee4cda6873c27643f78a14f3b
# Parent  47f1b099497c9a74d3496ef5894cee3e421a60e1
more command-line options;

diff -r 47f1b099497c -r d858e6f15da3 NEWS
--- a/NEWS	Thu Jan 05 22:30:20 2023 +0100
+++ b/NEWS	Fri Jan 06 12:05:32 2023 +0100
@@ -193,8 +193,8 @@
 
 * The command-line tool "isabelle update" is now directly based on
 "isabelle build" instead of "isabelle dump". Thus it has become more
-scalable, and supports a few additional options from "isabelle build".
-Partial builds are supported as well, e.g. "isabelle update -n -a".
+scalable, and supports most options from "isabelle build". Partial
+builds are supported as well, e.g. "isabelle update -n -a".
 
 * Isabelle/Scala provides generic support for XZ and Zstd compression,
 via Compress.Options and Compress.Cache. Bytes.uncompress automatically
diff -r 47f1b099497c -r d858e6f15da3 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Jan 05 22:30:20 2023 +0100
+++ b/src/Doc/System/Sessions.thy	Fri Jan 06 12:05:32 2023 +0100
@@ -476,10 +476,10 @@
   Option \<^verbatim>\<open>-f\<close> forces a fresh build of all selected sessions and their
   requirements.
 
-  \<^medskip>
-  Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
-  (including optional cleanup). Note that the return code always indicates the
-  status of the set of selected sessions.
+  \<^medskip> Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
+  (including optional cleanup). The overall return code always the status of
+  the set of selected sessions. Add-on builds (like presentation) are run for
+  successful sessions, i.e.\ already finished ones.
 
   \<^medskip>
   Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
@@ -784,7 +784,10 @@
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b           build heap images
+    -c           clean build
     -d DIR       include session directory
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -l NAME      additional base logic
@@ -794,26 +797,15 @@
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
-  Update theory sources based on PIDE markup.\<close>}
+  Update theory sources based on PIDE markup produced by "isabelle build".\<close>}
 
-  \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> and the
-  remaining command-line arguments specify sessions as in @{tool build}
-  (\secref{sec:tool-build}).
-
-  \<^medskip> Options \<^verbatim>\<open>-N\<close> and \<^verbatim>\<open>-j\<close> specify multicore parameters as in @{tool build}.
-
-  \<^medskip> Option \<^verbatim>\<open>-n\<close> suppresses the actual build process, but existing build
-  databases are used nonetheless.
+  \<^medskip> Most options are the same as for @{tool build} (\secref{sec:tool-build}).
 
   \<^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.
-
-  \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
-  (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
-  options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
-  ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
+  \<^medskip> Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> options, by relying on naming
+  convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
 
   \<^medskip> The following \<^verbatim>\<open>update\<close> options are supported:
 
diff -r 47f1b099497c -r d858e6f15da3 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Thu Jan 05 22:30:20 2023 +0100
+++ b/src/Pure/Tools/update.scala	Fri Jan 06 12:05:32 2023 +0100
@@ -12,10 +12,13 @@
     selection: Sessions.Selection = Sessions.Selection.empty,
     base_logics: List[String] = Nil,
     progress: Progress = new Progress,
+    build_heap: Boolean = false,
+    clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
+    fresh_build: Boolean = false,
     no_build: Boolean = false,
     verbose: Boolean = false
   ): Build.Results = {
@@ -117,7 +120,10 @@
         var requirements = false
         var exclude_session_groups: List[String] = Nil
         var all_sessions = false
+        var build_heap = false
+        var clean_build = false
         var dirs: List[Path] = Nil
+        var fresh_build = false
         var session_groups: List[String] = Nil
         var max_jobs = 1
         var base_logics: List[String] = Nil
@@ -135,7 +141,10 @@
     -R           refer to requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
+    -b           build heap images
+    -c           clean build
     -d DIR       include session directory
+    -f           fresh build
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
     -l NAME      additional base logic
@@ -145,7 +154,7 @@
     -v           verbose
     -x NAME      exclude session NAME and all descendants
 
-  Update theory sources based on PIDE markup.
+  Update theory sources based on PIDE markup produced by "isabelle build".
 """,
         "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
         "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
@@ -153,7 +162,10 @@
         "R" -> (_ => requirements = true),
         "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
         "a" -> (_ => all_sessions = true),
+        "b" -> (_ => build_heap = true),
+        "c" -> (_ => clean_build = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+        "f" -> (_ => fresh_build = true),
         "g:" -> (arg => session_groups = session_groups ::: List(arg)),
         "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
         "l:" -> (arg => base_logics ::= arg),
@@ -180,10 +192,13 @@
                 sessions = sessions),
               base_logics = base_logics,
               progress = progress,
+              build_heap,
+              clean_build,
               dirs = dirs,
               select_dirs = select_dirs,
               numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
               max_jobs = max_jobs,
+              fresh_build,
               no_build = no_build,
               verbose = verbose)
           }