--- a/etc/build.props Thu Jun 06 22:13:10 2024 +0200
+++ b/etc/build.props Thu Jun 06 22:34:24 2024 +0200
@@ -231,12 +231,12 @@
src/Pure/Tools/spell_checker.scala \
src/Pure/Tools/sync.scala \
src/Pure/Tools/task_statistics.scala \
- src/Pure/Tools/update.scala \
src/Pure/Tools/update_cartouches.scala \
src/Pure/Tools/update_comments.scala \
src/Pure/Tools/update_header.scala \
src/Pure/Tools/update_then.scala \
src/Pure/Tools/update_theorems.scala \
+ src/Pure/Tools/update_tool.scala \
src/Pure/library.scala \
src/Pure/name.scala \
src/Pure/pure_thy.scala \
--- a/src/Pure/System/isabelle_tool.scala Thu Jun 06 22:13:10 2024 +0200
+++ b/src/Pure/System/isabelle_tool.scala Thu Jun 06 22:34:24 2024 +0200
@@ -154,12 +154,12 @@
Server.isabelle_tool,
Sessions.isabelle_tool,
Sync.isabelle_tool,
- Update.isabelle_tool,
Update_Cartouches.isabelle_tool,
Update_Comments.isabelle_tool,
Update_Header.isabelle_tool,
Update_Then.isabelle_tool,
Update_Theorems.isabelle_tool,
+ Update_Tool.isabelle_tool,
isabelle.mirabelle.Mirabelle.isabelle_tool,
isabelle.vscode.Language_Server.isabelle_tool,
isabelle.vscode.VSCode_Main.isabelle_tool)
--- 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)
- })
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_tool.scala Thu Jun 06 22:34:24 2024 +0200
@@ -0,0 +1,232 @@
+/* Title: Pure/Tools/update_tool.scala
+ Author: Makarius
+
+Update theory sources based on PIDE markup.
+*/
+
+package isabelle
+
+
+object Update_Tool {
+ 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)
+ })
+}