treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
--- a/src/Doc/System/Sessions.thy Fri Jan 06 12:05:32 2023 +0100
+++ b/src/Doc/System/Sessions.thy Fri Jan 06 13:06:03 2023 +0100
@@ -793,7 +793,7 @@
-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"
+ -u OPT override "update" option for selected sessions
-v verbose
-x NAME exclude session NAME and all descendants
--- a/src/Pure/Thy/sessions.scala Fri Jan 06 12:05:32 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jan 06 13:06:03 2023 +0100
@@ -230,6 +230,7 @@
Info.make(
Chapter_Defs.empty,
info.options,
+ augment_options = _ => Nil,
dir_selected = false,
dir = Path.explode("$ISABELLE_TMP_PREFIX"),
chapter = info.chapter,
@@ -560,6 +561,7 @@
def make(
chapter_defs: Chapter_Defs,
options: Options,
+ augment_options: String => List[Options.Spec],
dir_selected: Boolean,
dir: Path,
chapter: String,
@@ -575,7 +577,8 @@
val session_path = dir + Path.explode(entry.path)
val directories = entry.directories.map(dir => session_path + Path.explode(dir))
- val session_options = options ++ entry.options
+ val entry_options = entry.options ::: augment_options(name)
+ val session_options = options ++ entry_options
val theories =
entry.theories.map({ case (opts, thys) =>
@@ -610,7 +613,7 @@
val meta_digest =
SHA1.digest(
- (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
+ (name, chapter, entry.parent, entry.directories, entry_options, entry.imports,
entry.theories_no_position, conditions, entry.document_theories_no_position,
entry.document_files)
.toString)
@@ -756,6 +759,7 @@
def make(
options: Options,
+ augment_options: String => List[Options.Spec] = _ => Nil,
roots: List[Root_File] = Nil,
infos: List[Info] = Nil
): Structure = {
@@ -775,7 +779,9 @@
root.entries.foreach {
case entry: Chapter_Entry => chapter = entry.name
case entry: Session_Entry =>
- root_infos += Info.make(chapter_defs, options, root.select, root.dir, chapter, entry)
+ root_infos +=
+ Info.make(chapter_defs, options, augment_options,
+ root.select, root.dir, chapter, entry)
case _ =>
}
chapter = UNSORTED
@@ -1262,10 +1268,11 @@
options: Options,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
- infos: List[Info] = Nil
+ infos: List[Info] = Nil,
+ augment_options: String => List[Options.Spec] = _ => Nil
): Structure = {
val roots = load_root_files(dirs = dirs, select_dirs = select_dirs)
- Structure.make(options, roots = roots, infos = infos)
+ Structure.make(options, augment_options, roots = roots, infos = infos)
}
--- a/src/Pure/Tools/build.scala Fri Jan 06 12:05:32 2023 +0100
+++ b/src/Pure/Tools/build.scala Fri Jan 06 13:06:03 2023 +0100
@@ -188,6 +188,7 @@
soft_build: Boolean = false,
verbose: Boolean = false,
export_files: Boolean = false,
+ augment_options: String => List[Options.Spec] = _ => Nil,
session_setup: (String, Session) => Unit = (_, _) => ()
): Results = {
val build_options =
@@ -204,7 +205,8 @@
/* session selection and dependencies */
val full_sessions =
- Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
+ Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos,
+ augment_options = augment_options)
val full_sessions_selection = full_sessions.imports_selection(selection)
def sources_stamp(deps: Sessions.Deps, session_name: String): String = {
--- a/src/Pure/Tools/update.scala Fri Jan 06 12:05:32 2023 +0100
+++ b/src/Pure/Tools/update.scala Fri Jan 06 13:06:03 2023 +0100
@@ -9,6 +9,7 @@
object Update {
def update(options: Options,
+ update_options: List[Options.Spec],
selection: Sessions.Selection = Sessions.Selection.empty,
base_logics: List[String] = Nil,
progress: Progress = new Progress,
@@ -38,13 +39,19 @@
sessions.build_requirements(base_logics).toSet
}
+ // test
+ options ++ update_options
+
+ def augment_options(name: String): List[Options.Spec] =
+ if (exclude(name)) Nil else update_options
+
/* build */
val build_results =
Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
selection = selection, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
- no_build = no_build, verbose = verbose)
+ no_build = no_build, verbose = verbose, augment_options = augment_options)
val store = build_results.store
val sessions_structure = build_results.deps.sessions_structure
@@ -129,6 +136,7 @@
var base_logics: List[String] = Nil
var no_build = false
var options = Options.init()
+ var update_options: List[Options.Spec] = Nil
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -150,7 +158,7 @@
-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"
+ -u OPT override "update" option for selected sessions
-v verbose
-x NAME exclude session NAME and all descendants
@@ -171,7 +179,7 @@
"l:" -> (arg => base_logics ::= arg),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
- "u:" -> (arg => options = options + ("update_" + arg)),
+ "u:" -> (arg => update_options = update_options ::: List(("update_" + arg, None))),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
@@ -181,7 +189,7 @@
val results =
progress.interrupt_handler {
- update(options,
+ update(options, update_options,
selection = Sessions.Selection(
requirements = requirements,
all_sessions = all_sessions,