# HG changeset patch # User wenzelm # Date 1673006763 -3600 # Node ID da13da82f6f95c94da6664a05891c6f5636be554 # Parent d858e6f15da3e6fee4cda6873c27643f78a14f3b treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions; diff -r d858e6f15da3 -r da13da82f6f9 src/Doc/System/Sessions.thy --- 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 diff -r d858e6f15da3 -r da13da82f6f9 src/Pure/Thy/sessions.scala --- 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) } diff -r d858e6f15da3 -r da13da82f6f9 src/Pure/Tools/build.scala --- 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 = { diff -r d858e6f15da3 -r da13da82f6f9 src/Pure/Tools/update.scala --- 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,