# HG changeset patch # User wenzelm # Date 1672946741 -3600 # Node ID 19be7d89bf0318d1cfc40bda9d575d84bfd37eb2 # Parent 302bdbb3bc05ed2652db56d94d6f460194c33bdb isabelle update no longer uses PIDE dump, but regular session build database: more scalable; misc tuning and clarification; diff -r 302bdbb3bc05 -r 19be7d89bf03 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Thu Jan 05 20:13:04 2023 +0100 +++ b/src/Pure/Tools/update.scala Thu Jan 05 20:25:41 2023 +0100 @@ -8,20 +8,45 @@ object Update { - def update(options: Options, logic: String, + def update(options: Options, + base_logics: List[String] = Nil, progress: Progress = new Progress, - log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, selection: Sessions.Selection = Sessions.Selection.empty - ): Unit = { - val context = - Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs, - selection = selection, skip_base = true) + ): Build.Results = { + /* excluded sessions */ + + val exclude: Set[String] = + if (base_logics.isEmpty) Set.empty + else { + val sessions = + Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs) + .selection(selection) + + for (name <- base_logics if !sessions.defined(name)) { + error("Base logic " + quote(name) + " outside of session selection") + } + + sessions.build_requirements(base_logics).toSet + } - context.build_logic(logic) + + /* build */ + + val build_results = + Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs, + selection = selection) - val path_cartouches = context.options.bool("update_path_cartouches") + if (!build_results.ok) error("Build failed") + + val store = build_results.store + val sessions_structure = build_results.deps.sessions_structure + + + /* update */ + + val path_cartouches = options.bool("update_path_cartouches") def update_xml(xml: XML.Body): XML.Body = xml flatMap { @@ -37,25 +62,40 @@ case t => List(t) } - context.sessions(logic, log = log).foreach(_.process { (args: Dump.Args) => - progress.echo("Processing theory " + args.print_node + " ...") + var seen_theory = Set.empty[String] - val snapshot = args.snapshot - for (node_name <- snapshot.node_files) { - val node = snapshot.get_node(node_name) - val xml = - snapshot.state.xml_markup(snapshot.version, node_name, - elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)) - - val source1 = Symbol.encode(XML.content(update_xml(xml))) - if (source1 != Symbol.encode(node.source)) { - progress.echo("Updating " + node_name.path) - File.write(node_name.path, source1) + using(Export.open_database_context(store)) { database_context => + for (session <- sessions_structure.build_topological_order if !exclude(session)) { + using(database_context.open_session0(session)) { session_context => + for { + db <- session_context.session_db() + theory <- store.read_theories(db, session) + if !seen_theory(theory) + } { + seen_theory += theory + val theory_context = session_context.theory(theory) + for { + theory_snapshot <- Build_Job.read_theory(theory_context) + node_name <- theory_snapshot.node_files + snapshot = theory_snapshot.switch(node_name) + if snapshot.node.is_wellformed_text + } { + progress.expose_interrupt() + val source1 = + XML.content(update_xml( + snapshot.xml_markup(elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)))) + if (source1 != snapshot.node.source) { + val path = Path.explode(node_name.node) + progress.echo("Updating " + quote(File.standard_path(path))) + File.write(path, source1) + } + } + } } } - }) + } - context.check_errors + build_results } @@ -71,7 +111,7 @@ var all_sessions = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil - var logic = Dump.default_logic + var base_logics: List[String] = Nil var options = Options.init() var verbose = false var exclude_sessions: List[String] = Nil @@ -85,7 +125,7 @@ -R refer to 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) + """) + -b NAME additional base logic -d DIR include session directory -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) @@ -100,7 +140,7 @@ "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), - "b:" -> (arg => logic = arg), + "b:" -> (arg => base_logics ::= arg), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "o:" -> (arg => options = options + arg), @@ -112,19 +152,23 @@ val progress = new Console_Progress(verbose = verbose) - progress.interrupt_handler { - update(options, logic, - progress = progress, - dirs = dirs, - select_dirs = select_dirs, - selection = Sessions.Selection( - requirements = requirements, - all_sessions = all_sessions, - base_sessions = base_sessions, - exclude_session_groups = exclude_session_groups, - exclude_sessions = exclude_sessions, - session_groups = session_groups, - sessions = sessions)) - } + val results = + progress.interrupt_handler { + update(options, + base_logics = base_logics, + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions)) + } + + sys.exit(results.rc) }) }