--- a/src/Pure/Tools/update.scala Thu Jun 06 22:13:10 2024 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-/* Title: Pure/Tools/update.scala
- Author: Makarius
-
-Update theory sources based on PIDE markup.
-*/
-
-package isabelle
-
-
-object Update {
- val update_elements: Markup.Elements =
- Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)
-
- def update_xml(options: Options, xml: XML.Body): XML.Body = {
- val update_path_cartouches = options.bool("update_path_cartouches")
- val update_cite = options.bool("update_cite")
- val cite_commands = Bibtex.cite_commands(options)
-
- def upd(lang: Markup.Language, ts: XML.Body): XML.Body =
- ts flatMap {
- case XML.Wrapped_Elem(markup, body1, body2) =>
- val body = if (markup.name == Markup.UPDATE) body1 else body2
- upd(lang, body)
- case XML.Elem(Markup.Language(lang1), body) =>
- if (update_path_cartouches && lang1.is_path) {
- Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
- case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
- case None => upd(lang1, body)
- }
- }
- else if (update_cite && lang1.is_antiquotation) {
- List(XML.Text(Bibtex.update_cite_antiquotation(cite_commands, XML.content(body))))
- }
- else upd(lang1, body)
- case XML.Elem(_, body) => upd(lang, body)
- case XML.Text(s) if update_cite && lang.is_document =>
- List(XML.Text(Bibtex.update_cite_commands(s)))
- case t => List(t)
- }
- upd(Markup.Language.outer, xml)
- }
-
- def default_base_logic: String = Isabelle_System.getenv("ISABELLE_LOGIC")
-
- def update(options: Options,
- update_options: List[Options.Spec],
- 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: Option[Int] = None,
- fresh_build: Boolean = false,
- no_build: Boolean = false
- ): Build.Results = {
- /* excluded sessions */
-
- val exclude: Set[String] =
- if (base_logics.isEmpty) Set.empty
- else {
- Sessions.load_structure(options, dirs = dirs ::: select_dirs)
- .selection(Sessions.Selection(sessions = base_logics))
- .build_graph.domain
- }
-
- // test
- options ++ update_options
-
- def augment_options(name: String): List[Options.Spec] =
- if (exclude(name)) Nil else update_options
-
-
- /* build */
-
- val build_options = options + "build_thorough"
-
- val build_results =
- Build.build(build_options, progress = progress, dirs = dirs, select_dirs = select_dirs,
- selection = selection, build_heap = build_heap, clean_build = clean_build,
- numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
- no_build = no_build, augment_options = augment_options)
-
- val store = build_results.store
- val sessions_structure = build_results.deps.sessions_structure
-
-
- /* update */
-
- var seen_theory = Set.empty[String]
-
- using(Export.open_database_context(store)) { database_context =>
- for {
- session <- sessions_structure.build_topological_order
- if build_results(session).ok && !exclude(session)
- } {
- progress.echo("Updating " + session + " ...")
- val session_options = sessions_structure(session).options
- val proper_session_theory =
- build_results.deps(session).proper_session_theories.map(_.theory).toSet
- using(database_context.open_session0(session)) { session_context =>
- for {
- db <- session_context.session_db()
- theory <- store.read_theories(db, session)
- if proper_session_theory(theory) && !seen_theory(theory)
- } {
- seen_theory += theory
- val theory_context = session_context.theory(theory)
- for {
- theory_snapshot <- Build.read_theory(theory_context)
- node_name <- theory_snapshot.node_files
- snapshot = theory_snapshot.switch(node_name)
- if snapshot.node.source_wellformed
- } {
- progress.expose_interrupt()
- val xml = YXML.parse_body(YXML.string_of_body(snapshot.xml_markup(elements = update_elements)))
- val source1 = XML.content(update_xml(session_options, xml))
- if (source1 != snapshot.node.source) {
- val path = Path.explode(node_name.node)
- progress.echo("File " + quote(File.standard_path(path)))
- File.write(path, source1)
- }
- }
- }
- }
- }
- }
-
- build_results
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here,
- { args =>
- var base_sessions: List[String] = Nil
- var select_dirs: List[Path] = Nil
- var numa_shuffling = false
- 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: Option[Int] = None
- var base_logics: List[String] = List(default_base_logic)
- var no_build = false
- var options = Options.init()
- var update_options: List[Options.Spec] = Nil
- var verbose = false
- var exclude_sessions: List[String] = Nil
-
- val getopts = Getopts("""
-Usage: isabelle update [OPTIONS] [SESSIONS ...]
-
- Options are:
- -B NAME include session NAME and all descendants
- -D DIR include session directory and select its sessions
- -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 NAMES comma-separated list of base logics, to remain unchanged
- (default: """ + quote(default_base_logic) + """)
- -n no build -- take existing session build databases
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -u OPT override "update" option for selected sessions
- -v verbose
- -x NAME exclude session NAME and all descendants
-
- 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))),
- "N" -> (_ => numa_shuffling = true),
- "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 = Some(Value.Nat.parse(arg))),
- "l:" -> (arg => base_logics = space_explode(',', arg)),
- "n" -> (_ => no_build = true),
- "o:" -> (arg => options = options + arg),
- "u:" -> (arg => update_options = update_options ::: List(Options.Spec("update_" + arg))),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
-
- val sessions = getopts(args)
-
- val progress = new Console_Progress(verbose = verbose)
-
- val results =
- progress.interrupt_handler {
- update(options, update_options,
- 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),
- base_logics = base_logics,
- progress = progress,
- build_heap = build_heap,
- clean_build = clean_build,
- dirs = dirs,
- select_dirs = select_dirs,
- numa_shuffling = Host.numa_check(progress, numa_shuffling),
- max_jobs = max_jobs,
- fresh_build = fresh_build,
- no_build = no_build)
- }
-
- sys.exit(results.rc)
- })
-}