# HG changeset patch # User paulson # Date 1673284582 0 # Node ID 5e033f907bcc0948a4d5d623e1b56d67f21747e8 # Parent 2e849cebd65efb6b5a89264c9143a20228564821# Parent 711cef61c0ce1690d8cda6a8760cf3570165a9da merged diff -r 711cef61c0ce -r 5e033f907bcc NEWS --- a/NEWS Mon Jan 09 17:16:04 2023 +0000 +++ b/NEWS Mon Jan 09 17:16:22 2023 +0000 @@ -191,6 +191,11 @@ *** System *** +* The command-line tool "isabelle update" is now directly based on +"isabelle build" instead of "isabelle dump". Thus it has become more +scalable, and supports most options from "isabelle build". Partial +builds are supported as well, e.g. "isabelle update -n -a". + * Isabelle/Scala provides generic support for XZ and Zstd compression, via Compress.Options and Compress.Cache. Bytes.uncompress automatically detects the compression scheme. diff -r 711cef61c0ce -r 5e033f907bcc src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Jan 09 17:16:22 2023 +0000 @@ -1324,8 +1324,8 @@ files as for \<^theory_text>\export_generated_files\ and writes them into a temporary directory, which is taken as starting point for build process of Isabelle/Scala/Java modules (see @{cite "isabelle-system"}). The - corresponding @{path build.props} file is expected directly in the toplevel - directory, instead of @{path "etc/build.props"} for Isabelle system + corresponding @{path \build.props\} file is expected directly in the toplevel + directory, instead of @{path \etc/build.props\} for Isabelle system components. These properties need to specify sources, resources, services etc. as usual. The resulting JAR module becomes an export artefact of the session database, with a name of the form diff -r 711cef61c0ce -r 5e033f907bcc src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Doc/System/Sessions.thy Mon Jan 09 17:16:22 2023 +0000 @@ -375,7 +375,7 @@ -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files - -n no build -- test dependencies only + -n no build -- take existing build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants @@ -476,10 +476,10 @@ Option \<^verbatim>\-f\ forces a fresh build of all selected sessions and their requirements. - \<^medskip> - Option \<^verbatim>\-n\ omits the actual build process after the preparatory stage - (including optional cleanup). Note that the return code always indicates the - status of the set of selected sessions. + \<^medskip> Option \<^verbatim>\-n\ omits the actual build process after the preparatory stage + (including optional cleanup). The overall return code always the status of + the set of selected sessions. Add-on builds (like presentation) are run for + successful sessions, i.e.\ already finished ones. \<^medskip> Option \<^verbatim>\-j\ specifies the maximum number of parallel build jobs (prover @@ -774,8 +774,8 @@ text \ The @{tool_def "update"} tool updates theory sources based on markup that is - produced from a running PIDE session (similar to @{tool dump} - \secref{sec:tool-dump}). Its command-line usage is: @{verbatim [display] + produced by the regular @{tool build} process \secref{sec:tool-build}). Its + command-line usage is: @{verbatim [display] \Usage: isabelle update [OPTIONS] [SESSIONS ...] Options are: @@ -784,30 +784,28 @@ -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 "Pure") + -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 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 - Update theory sources based on PIDE markup.\} + Update theory sources based on PIDE markup produced by "isabelle build".\} - \<^medskip> Options \<^verbatim>\-B\, \<^verbatim>\-D\, \<^verbatim>\-R\, \<^verbatim>\-X\, \<^verbatim>\-a\, \<^verbatim>\-d\, \<^verbatim>\-g\, \<^verbatim>\-x\ and the - remaining command-line arguments specify sessions as in @{tool build} - (\secref{sec:tool-build}) or @{tool dump} (\secref{sec:tool-dump}). + \<^medskip> Most options are the same as for @{tool build} (\secref{sec:tool-build}). - \<^medskip> Option \<^verbatim>\-b\ specifies an optional base logic image, for improved - scalability of the PIDE session. Its theories are only processed if it is - included in the overall session selection. + \<^medskip> Option \<^verbatim>\-l\ specifies one or more base logics: these sessions and their + ancestors are \<^emph>\excluded\ from the update. - \<^medskip> Option \<^verbatim>\-v\ increases the general level of verbosity. - - \<^medskip> Option \<^verbatim>\-o\ overrides Isabelle system options as for @{tool build} - (\secref{sec:tool-build}). Option \<^verbatim>\-u\ refers to specific \<^verbatim>\update\ - options, by relying on naming convention: ``\<^verbatim>\-u\~\OPT\'' is a shortcut for - ``\<^verbatim>\-o\~\<^verbatim>\update_\\OPT\''. + \<^medskip> Option \<^verbatim>\-u\ refers to specific \<^verbatim>\update\ options, by relying on naming + convention: ``\<^verbatim>\-u\~\OPT\'' is a shortcut for ``\<^verbatim>\-o\~\<^verbatim>\update_\\OPT\''. \<^medskip> The following \<^verbatim>\update\ options are supported: @@ -850,20 +848,14 @@ @{verbatim [display] \ isabelle update -u mixfix_cartouches HOL-Analysis\} - \<^smallskip> Update the same for all application sessions based on \<^verbatim>\HOL-Analysis\ --- - using its image as starting point (for reduced resource requirements): - - @{verbatim [display] \ isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\} + \<^smallskip> Update the same for all application sessions based on \<^verbatim>\HOL-Analysis\, but + do not change the underlying \<^verbatim>\HOL\ (and \<^verbatim>\Pure\) session: - \<^smallskip> Update sessions that build on \<^verbatim>\HOL-Proofs\, which need to be run - separately with special options as follows: + @{verbatim [display] \ isabelle update -u mixfix_cartouches -l HOL -B HOL-Analysis\} - @{verbatim [display] \ isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs - -o record_proofs=2\} + \<^smallskip> Update all sessions that happen to be properly built beforehand: - \<^smallskip> See also the end of \secref{sec:tool-dump} for hints on increasing - Isabelle/ML heap sizes for very big PIDE processes that include many - sessions, notably from the Archive of Formal Proofs. + @{verbatim [display] \ isabelle update -u mixfix_cartouches -n -a\} \ diff -r 711cef61c0ce -r 5e033f907bcc src/HOL/Analysis/Metric_Arith.thy --- a/src/HOL/Analysis/Metric_Arith.thy Mon Jan 09 17:16:04 2023 +0000 +++ b/src/HOL/Analysis/Metric_Arith.thy Mon Jan 09 17:16:22 2023 +0000 @@ -105,7 +105,7 @@ "x \ s \ y \ s \ x = y \ (\a\s. dist x a = dist y a)" by auto -ML_file "metric_arith.ML" +ML_file \metric_arith.ML\ method_setup metric = \ Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac) diff -r 711cef61c0ce -r 5e033f907bcc src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Mon Jan 09 17:16:04 2023 +0000 +++ b/src/HOL/Quotient.thy Mon Jan 09 17:16:22 2023 +0000 @@ -870,7 +870,7 @@ unfolding Quotient_def eq_onp_def by unfold_locales auto -ML_file "Tools/BNF/bnf_lift.ML" +ML_file \Tools/BNF/bnf_lift.ML\ hide_fact sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Isar/document_structure.scala --- a/src/Pure/Isar/document_structure.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Isar/document_structure.scala Mon Jan 09 17:16:22 2023 +0000 @@ -99,7 +99,7 @@ /* result structure */ val spans = syntax.parse_spans(text) - spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.none, span))) + spans.foreach(span => add(Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span))) result() } @@ -166,7 +166,7 @@ for { span <- syntax.parse_spans(text) } { sections.add( new Command_Item(syntax.keywords, - Command(Document_ID.none, node_name, Command.Blobs_Info.none, span))) + Command(Document_ID.none, node_name, Command.Blobs_Info.empty, span))) } sections.result() } diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/PIDE/command.scala Mon Jan 09 17:16:22 2023 +0000 @@ -14,27 +14,20 @@ object Command { /* blobs */ - object Blob { - def read_file(name: Document.Node.Name, src_path: Path): Blob = { - val bytes = Bytes.read(name.path) - val chunk = Symbol.Text_Chunk(bytes.text) - Blob(name, src_path, Some((bytes.sha1_digest, chunk))) - } - } - sealed case class Blob( name: Document.Node.Name, src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)] ) { - def read_file: Bytes = Bytes.read(name.path) - def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node) } object Blobs_Info { - val none: Blobs_Info = Blobs_Info(Nil) + val empty: Blobs_Info = Blobs_Info(Nil) + + def make(blobs: List[(Blob, Document.Blobs.Item)]): Blobs_Info = + if (blobs.isEmpty) empty else Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a)) def errors(msgs: List[String]): Blobs_Info = Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg)))) @@ -119,6 +112,7 @@ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file) + def make(blobs: List[Blob]): List[Markup_Index] = markup :: blobs.map(blob) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) @@ -377,14 +371,14 @@ } val empty: Command = - Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty) + Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.empty, Command_Span.empty) def unparsed( source: String, theory: Boolean = false, id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, - blobs_info: Blobs_Info = Blobs_Info.none, + blobs_info: Blobs_Info = Blobs_Info.empty, results: Results = Results.empty, markups: Markups = Markups.empty ): Command = { @@ -428,7 +422,7 @@ def blobs_info( resources: Resources, syntax: Outer_Syntax, - get_blob: Document.Node.Name => Option[Document.Blob], + get_blob: Document.Node.Name => Option[Document.Blobs.Item], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/PIDE/document.scala Mon Jan 09 17:16:22 2023 +0000 @@ -41,17 +41,27 @@ /* document blobs: auxiliary files */ - sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) { - def unchanged: Blob = copy(changed = false) + object Blobs { + sealed case class Item( + bytes: Bytes, + source: String, + chunk: Symbol.Text_Chunk, + changed: Boolean + ) { + def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty + def unchanged: Item = copy(changed = false) + } + + def apply(blobs: Map[Node.Name, Item]): Blobs = new Blobs(blobs) + val empty: Blobs = apply(Map.empty) + + def make(blobs: List[(Command.Blob, Item)]): Blobs = + if (blobs.isEmpty) empty + else apply((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap) } - object Blobs { - def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs) - val empty: Blobs = apply(Map.empty) - } - - final class Blobs private(blobs: Map[Node.Name, Blob]) { - def get(name: Node.Name): Option[Blob] = blobs.get(name) + final class Blobs private(blobs: Map[Node.Name, Blobs.Item]) { + def get(name: Node.Name): Option[Blobs.Item] = blobs.get(name) def changed(name: Node.Name): Boolean = get(name) match { @@ -93,7 +103,7 @@ object Name { def apply(node: String, theory: String = ""): Name = new Name(node, theory) - def loaded_theory(theory: String): Document.Node.Name = Name(theory, theory = theory) + def loaded_theory(theory: String): Name = Name(theory, theory = theory) val empty: Name = Name("") @@ -171,7 +181,7 @@ case _ => false } } - case class Blob[A, B](blob: Document.Blob) extends Edit[A, B] + case class Blob[A, B](blob: Blobs.Item) extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] @@ -263,10 +273,13 @@ } val empty: Node = new Node() + + def init_blob(blob: Blobs.Item): Node = + new Node(get_blob = Some(blob.unchanged)) } final class Node private( - val get_blob: Option[Document.Blob] = None, + val get_blob: Option[Blobs.Item] = None, val header: Node.Header = Node.no_header, val syntax: Option[Outer_Syntax] = None, val text_perspective: Text.Perspective = Text.Perspective.empty, @@ -292,8 +305,6 @@ def load_commands_changed(doc_blobs: Blobs): Boolean = load_commands.exists(_.blobs_changed(doc_blobs)) - def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged)) - def update_header(new_header: Node.Header): Node = new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands) @@ -332,6 +343,12 @@ def command_start(cmd: Command): Option[Text.Offset] = Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2) + lazy val source_wellformed: Boolean = + get_blob match { + case Some(blob) => blob.source_wellformed + case None => true + } + lazy val source: String = get_blob match { case Some(blob) => blob.source @@ -517,16 +534,16 @@ final class Pending_Edits(pending_edits: Map[Node.Name, List[Text.Edit]]) { def is_stable: Boolean = pending_edits.isEmpty - def + (entry: (Document.Node.Name, List[Text.Edit])): Pending_Edits = { + def + (entry: (Node.Name, List[Text.Edit])): Pending_Edits = { val (name, es) = entry if (es.isEmpty) this else new Pending_Edits(pending_edits + (name -> (es ::: edits(name)))) } - def edits(name: Document.Node.Name): List[Text.Edit] = + def edits(name: Node.Name): List[Text.Edit] = pending_edits.getOrElse(name, Nil) - def reverse_edits(name: Document.Node.Name): List[Text.Edit] = + def reverse_edits(name: Node.Name): List[Text.Edit] = reverse_pending_edits.getOrElse(name, Nil) private lazy val reverse_pending_edits = @@ -563,15 +580,6 @@ node_name :: node.load_commands.flatMap(_.blobs_names) - /* source text */ - - def source: String = - snippet_command match { - case Some(command) => command.source - case None => node.source - } - - /* pending edits */ def is_outdated: Boolean = !pending_edits.is_stable @@ -602,15 +610,19 @@ /* command as add-on snippet */ - def snippet(command: Command): Snapshot = { + def snippet(command: Command, doc_blobs: Blobs): Snapshot = { val node_name = command.node_name + val blobs = for (a <- command.blobs_names; b <- doc_blobs.get(a)) yield a -> b + val nodes0 = version.nodes val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) - val version1 = Document.Version.make(nodes1) + val nodes2 = blobs.foldLeft(nodes1) { case (ns, (a, b)) => ns + (a -> Node.init_blob(b)) } + val version1 = Version.make(nodes2) val edits: List[Edit_Text] = - List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) + List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) ::: + blobs.map({ case (a, b) => a -> Node.Blob(b) }) val state0 = state.define_command(command) val state1 = @@ -622,42 +634,17 @@ } - /* XML markup */ + /* markup and messages */ def xml_markup( range: Text.Range = Text.Range.full, elements: Markup.Elements = Markup.Elements.full): XML.Body = state.xml_markup(version, node_name, range = range, elements = elements) - def xml_markup_blobs( - elements: Markup.Elements = Markup.Elements.full - ) : List[(Command.Blob, XML.Body)] = { - snippet_command match { - case None => Nil - case Some(command) => - for (Exn.Res(blob) <- command.blobs) - yield { - val bytes = blob.read_file - val text = bytes.text - val xml = - if (Bytes(text) == bytes) { - val markup = command.init_markups(Command.Markup_Index.blob(blob)) - markup.to_XML(Text.Range.length(text), text, elements) - } - else Nil - blob -> xml - } - } - } - - - /* messages */ - lazy val messages: List[(XML.Elem, Position.T)] = (for { (command, start) <- - Document.Node.Commands.starts_pos( - node.commands.iterator, Token.Pos.file(node_name.node)) + Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node)) pos = command.span.keyword_pos(start).position(command.span.name) (_, elem) <- state.command_results(version, command).iterator } yield (elem, pos)).toList @@ -794,7 +781,7 @@ def node_required: Boolean - def get_blob: Option[Blob] + def get_blob: Option[Blobs.Item] def untyped_data: AnyRef def get_data[C](c: Class[C]): Option[C] = Library.as_subclass(c)(untyped_data) @@ -1003,17 +990,18 @@ } } - def end_theory(id: Document_ID.Exec): (Snapshot, State) = + def end_theory(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): (Snapshot, State) = theories.get(id) match { case None => fail case Some(st) => val command = st.command val node_name = command.node_name + val doc_blobs = document_blobs(node_name) val command1 = Command.unparsed(command.source, theory = true, id = id, node_name = node_name, blobs_info = command.blobs_info, results = st.results, markups = st.markups) val state1 = copy(theories = theories - id) - (state1.snippet(command1), state1) + (state1.snippet(command1, doc_blobs), state1) } def assign( @@ -1199,9 +1187,8 @@ tree <- markup.to_XML(command_range, command.source, elements).iterator } yield tree).toList } - else { + else if (node.source_wellformed) { Text.Range.length(node.source).try_restrict(range) match { - case None => Nil case Some(node_range) => val markup = version.nodes.commands_loading(node_name).headOption match { @@ -1212,8 +1199,10 @@ command_markup(version, command, markup_index, node_range, elements) } markup.to_XML(node_range, node.source, elements) + case None => Nil } } + else Nil } def node_initialized(version: Version, name: Node.Name): Boolean = @@ -1250,7 +1239,7 @@ new Snapshot(this, version, node_name, pending_edits1, snippet_command) } - def snippet(command: Command): Snapshot = - snapshot().snippet(command) + def snippet(command: Command, doc_blobs: Blobs): Snapshot = + snapshot().snippet(command, doc_blobs) } } diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/PIDE/headless.scala Mon Jan 09 17:16:22 2023 +0000 @@ -496,7 +496,7 @@ } sealed case class State( - blobs: Map[Document.Node.Name, Document.Blob] = Map.empty, + blobs: Map[Document.Node.Name, Document.Blobs.Item] = Map.empty, theories: Map[Document.Node.Name, Theory] = Map.empty, required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty ) { @@ -508,13 +508,12 @@ val new_blobs = names.flatMap { name => val bytes = Bytes.read(name.path) - def new_blob: Document.Blob = { - val text = bytes.text - Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true) - } blobs.get(name) match { - case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob) - case None => Some(name -> new_blob) + case Some(blob) if blob.bytes == bytes => None + case _ => + val text = bytes.text + val blob = Document.Blobs.Item(bytes, text, Symbol.Text_Chunk(text), changed = true) + Some(name -> blob) } } val blobs1 = new_blobs.foldLeft(blobs)(_ + _) @@ -524,7 +523,7 @@ def blob_edits( name: Document.Node.Name, - old_blob: Option[Document.Blob] + old_blob: Option[Document.Blobs.Item] ) : List[Document.Edit_Text] = { val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString))) val text_edits = diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/PIDE/session.scala Mon Jan 09 17:16:22 2023 +0000 @@ -125,8 +125,8 @@ val cache: Term.Cache = Term.Cache.make() - def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = - Command.Blobs_Info.none + def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.empty + def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty /* global flags */ @@ -560,7 +560,7 @@ case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { - val snapshot = global_state.change_result(_.end_theory(id)) + val snapshot = global_state.change_result(_.end_theory(id, build_blobs)) finished_theories.post(snapshot) } file_formats.stop_session() diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Pure.thy Mon Jan 09 17:16:22 2023 +0000 @@ -202,8 +202,8 @@ (Toplevel.context_of st) args external))); in end\ -external_file "ROOT0.ML" -external_file "ROOT.ML" +external_file \ROOT0.ML\ +external_file \ROOT.ML\ subsection \Embedded ML text\ diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/ROOT.ML Mon Jan 09 17:16:22 2023 +0000 @@ -366,3 +366,4 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML"; + diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Thy/bibtex.scala Mon Jan 09 17:16:22 2023 +0000 @@ -35,7 +35,7 @@ val title = "Bibliography " + quote(snapshot.node_name.file_name) val content = Isabelle_System.with_tmp_file("bib", "bib") { bib => - File.write(bib, snapshot.source) + File.write(bib, snapshot.node.source) Bibtex.html_output(List(bib), style = "unsort", title = title) } Some(Browser_Info.HTML_Document(title, content)) diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Thy/browser_info.scala --- a/src/Pure/Thy/browser_info.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Thy/browser_info.scala Mon Jan 09 17:16:22 2023 +0000 @@ -265,7 +265,7 @@ val name = snapshot.node_name if (plain_text) { val title = "File " + Symbol.cartouche_decoded(name.file_name) - val body = HTML.text(snapshot.source) + val body = HTML.text(snapshot.node.source) html_document(title, body, fonts_css) } else { @@ -614,23 +614,29 @@ node_context(theory.thy_file, session_dir). make_html(thy_elements, snapshot.xml_markup(elements = thy_elements.html))) + val master_dir = Path.explode(snapshot.node_name.master_dir) + val files = for { - (blob, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html) + blob_name <- snapshot.node_files.tail + xml = snapshot.switch(blob_name).xml_markup(elements = thy_elements.html) if xml.nonEmpty } yield { progress.expose_interrupt() - val file_name = blob.name.node - if (verbose) progress.echo("Presenting file " + quote(file_name)) + val file = blob_name.node + if (verbose) progress.echo("Presenting file " + quote(file)) - val file_html = session_dir + context.file_html(file_name) + val file_html = session_dir + context.file_html(file) val file_dir = file_html.dir val html_link = HTML.relative_href(file_html, base = Some(session_dir)) - val html = context.source(node_context(file_name, file_dir).make_html(thy_elements, xml)) + val html = context.source(node_context(file, file_dir).make_html(thy_elements, xml)) - val file_title = "File " + Symbol.cartouche_decoded(blob.src_path.implode_short) + val path = Path.explode(file) + val src_path = File.relative_path(master_dir, path).getOrElse(path) + + val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) HTML.write_document(file_dir, file_html.file_name, List(HTML.title(file_title)), List(context.head(file_title), html), root = Some(context.root_dir)) diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Thy/export.scala Mon Jan 09 17:16:22 2023 +0000 @@ -423,23 +423,16 @@ def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context = new Theory_Context(session_context, theory, other_cache) - def node_source(name: Document.Node.Name): String = { - def snapshot_source: Option[String] = - for { - snapshot <- document_snapshot - node = snapshot.get_node(name) - text = node.source if text.nonEmpty - } yield text - + def get_source_file(name: String): Option[Sessions.Source_File] = { val store = database_context.store - def db_source: Option[String] = - (for { - database <- db_hierarchy.iterator - file <- store.read_sources(database.db, database.session, name = name.node).iterator - } yield file.text).nextOption() + (for { + database <- db_hierarchy.iterator + file <- store.read_sources(database.db, database.session, name = name).iterator + } yield file).nextOption() + } - snapshot_source orElse db_source getOrElse "" - } + def source_file(name: String): Sessions.Source_File = + get_source_file(name).getOrElse(error("Missing session source file " + quote(name))) def classpath(): List[File.Content] = { (for { diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Thy/sessions.scala Mon Jan 09 17:16:22 2023 +0000 @@ -67,7 +67,6 @@ override def toString: String = name def bytes: Bytes = if (compressed) body.uncompress(cache = cache) else body - def text: String = bytes.text } object Sources { @@ -109,6 +108,10 @@ class Sources private(rep: Map[String, Source_File]) extends Iterable[Source_File] { override def toString: String = rep.values.toList.sortBy(_.name).mkString("Sources(", ", ", ")") override def iterator: Iterator[Source_File] = rep.valuesIterator + + def get(name: String): Option[Source_File] = rep.get(name) + def apply(name: String): Source_File = + get(name).getOrElse(error("Missing session sources entry " + quote(name))) } @@ -226,6 +229,7 @@ Info.make( Chapter_Defs.empty, info.options, + augment_options = _ => Nil, dir_selected = false, dir = Path.explode("$ISABELLE_TMP_PREFIX"), chapter = info.chapter, @@ -556,6 +560,7 @@ def make( chapter_defs: Chapter_Defs, options: Options, + augment_options: String => List[Options.Spec], dir_selected: Boolean, dir: Path, chapter: String, @@ -571,7 +576,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) => @@ -606,7 +612,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) @@ -752,6 +758,7 @@ def make( options: Options, + augment_options: String => List[Options.Spec] = _ => Nil, roots: List[Root_File] = Nil, infos: List[Info] = Nil ): Structure = { @@ -771,7 +778,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 @@ -1258,10 +1267,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 711cef61c0ce -r 5e033f907bcc src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Thy/thy_syntax.scala Mon Jan 09 17:16:22 2023 +0000 @@ -166,7 +166,7 @@ private def reparse_spans( resources: Resources, syntax: Outer_Syntax, - get_blob: Document.Node.Name => Option[Document.Blob], + get_blob: Document.Node.Name => Option[Document.Blobs.Item], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, commands: Linear_Set[Command], @@ -213,7 +213,7 @@ private def text_edit( resources: Resources, syntax: Outer_Syntax, - get_blob: Document.Node.Name => Option[Document.Blob], + get_blob: Document.Node.Name => Option[Document.Blobs.Item], can_import: Document.Node.Name => Boolean, reparse_limit: Int, node: Document.Node, @@ -245,7 +245,7 @@ } edit match { - case (_, Document.Node.Blob(blob)) => node.init_blob(blob) + case (_, Document.Node.Blob(blob)) => Document.Node.init_blob(blob) case (name, Document.Node.Edits(text_edits)) => if (name.is_theory) { @@ -303,7 +303,7 @@ ): Session.Change = { val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) - def get_blob(name: Document.Node.Name): Option[Document.Blob] = + def get_blob(name: Document.Node.Name): Option[Document.Blobs.Item] = doc_blobs.get(name) orElse previous.nodes(name).get_blob def can_import(name: Document.Node.Name): Boolean = diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Tools/build.scala Mon Jan 09 17:16:22 2023 +0000 @@ -139,8 +139,8 @@ class Results private[Build]( val store: Sessions.Store, val deps: Sessions.Deps, - results: Map[String, (Option[Process_Result], Sessions.Info)], - val presentation_sessions: Browser_Info.Config => List[String] + val sessions_ok: List[String], + results: Map[String, (Option[Process_Result], Sessions.Info)] ) { def cache: Term.Cache = store.cache @@ -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 = { @@ -452,18 +454,18 @@ } else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) } + val sessions_ok: List[String] = + (for { + name <- build_deps.sessions_structure.build_topological_order.iterator + result <- build_results.get(name) + if result.ok + } yield name).toList + val results = (for ((name, result) <- build_results.iterator) yield (name, (result.process, result.info))).toMap - def presentation_sessions(config: Browser_Info.Config): List[String] = - (for { - name <- build_deps.sessions_structure.build_topological_order.iterator - result <- build_results.get(name) - if result.ok && config.enabled(result.info) - } yield name).toList - - new Results(store, build_deps, results, presentation_sessions) + new Results(store, build_deps, sessions_ok, results) } if (export_files) { @@ -481,7 +483,8 @@ } } - val presentation_sessions = results.presentation_sessions(browser_info) + val presentation_sessions = + results.sessions_ok.filter(name => browser_info.enabled(results.info(name))) if (presentation_sessions.nonEmpty && !progress.stopped) { Browser_Info.build(browser_info, results.store, results.deps, presentation_sessions, progress = progress, verbose = verbose) @@ -545,7 +548,7 @@ -j INT maximum number of parallel jobs (default 1) -k KEYWORD check theory sources for conflicts with proposed keywords -l list session source files - -n no build -- test dependencies only + -n no build -- take existing build databases -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Tools/build_job.scala Mon Jan 09 17:16:22 2023 +0000 @@ -18,64 +18,66 @@ theory_context: Export.Theory_Context, unicode_symbols: Boolean = false ): Option[Document.Snapshot] = { + def decode_bytes(bytes: Bytes): String = + Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes)) + def read(name: String): Export.Entry = theory_context(name, permissive = true) def read_xml(name: String): XML.Body = - YXML.parse_body( - Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)), - cache = theory_context.cache) + YXML.parse_body(decode_bytes(read(name).bytes), cache = theory_context.cache) + + def read_source_file(name: String): Sessions.Source_File = + theory_context.session_context.source_file(name) for { id <- theory_context.document_id() (thy_file, blobs_files) <- theory_context.files(permissive = true) } yield { - val results = - Command.Results.make( - for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) - yield i -> elem) - val master_dir = Path.explode(Url.strip_base_name(thy_file).getOrElse( error("Cannot determine theory master directory: " + quote(thy_file)))) val blobs = - blobs_files.map { file => - val name = Document.Node.Name(file) - val path = Path.explode(file) + blobs_files.map { name => + val path = Path.explode(name) val src_path = File.relative_path(master_dir, path).getOrElse(path) - Command.Blob(name, src_path, None) + + val file = read_source_file(name) + val bytes = file.bytes + val text = decode_bytes(bytes) + val chunk = Symbol.Text_Chunk(text) + + Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) -> + Document.Blobs.Item(bytes, text, chunk, changed = false) } + + val thy_source = decode_bytes(read_source_file(thy_file).bytes) + val thy_xml = read_xml(Export.MARKUP) val blobs_xml = for (i <- (1 to blobs.length).toList) yield read_xml(Export.MARKUP + i) - val blobs_info = - Command.Blobs_Info( - for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml } - yield { - val text = XML.content(xml) - val chunk = Symbol.Text_Chunk(text) - val digest = SHA1.digest(Symbol.encode(text)) - Exn.Res(Command.Blob(name, src_path, Some((digest, chunk)))) - }) - - val thy_xml = read_xml(Export.MARKUP) - val thy_source = XML.content(thy_xml) - - val markups_index = - Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob) + val markups_index = Command.Markup_Index.make(blobs.map(_._1)) val markups = Command.Markups.make( for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) yield index -> Markup_Tree.from_XML(xml)) + val results = + Command.Results.make( + for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) + yield i -> elem) + val command = Command.unparsed(thy_source, theory = true, id = id, node_name = Document.Node.Name(thy_file, theory = theory_context.theory), - blobs_info = blobs_info, results = results, markups = markups) + blobs_info = Command.Blobs_Info.make(blobs), + markups = markups, results = results) - Document.State.init.snippet(command) + val doc_blobs = Document.Blobs.make(blobs) + + Document.State.init.snippet(command, doc_blobs) } } @@ -134,7 +136,7 @@ rendering.text_messages(Text.Range.full) .filter(message => verbose || Protocol.is_exported(message.info)) if (messages.nonEmpty) { - val line_document = Line.Document(snapshot.source) + val line_document = Line.Document(snapshot.node.source) val buffer = new mutable.ListBuffer[String] for (Text.Info(range, elem) <- messages) { val line = line_document.position(range.start).line1 @@ -269,30 +271,38 @@ } else Nil + def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] = + session_background.base.theory_load_commands.get(node_name.theory) match { + case None => Nil + case Some(spans) => + val syntax = session_background.base.theory_syntax(node_name) + val master_dir = Path.explode(node_name.master_dir) + for (span <- spans; file <- span.loaded_files(syntax).files) + yield { + val src_path = Path.explode(file) + val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path)) + + val bytes = session_sources(blob_name.node).bytes + val text = bytes.text + val chunk = Symbol.Text_Chunk(text) + + Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) -> + Document.Blobs.Item(bytes, text, chunk, changed = false) + } + } + val resources = new Resources(session_background, log = log, command_timings = command_timings0) + val session = new Session(options, resources) { override val cache: Term.Cache = store.cache - override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = { - session_background.base.theory_load_commands.get(node_name.theory) match { - case Some(spans) => - val syntax = session_background.base.theory_syntax(node_name) - val blobs = - for (span <- spans; file <- span.loaded_files(syntax).files) - yield { - (Exn.capture { - val master_dir = Path.explode(node_name.master_dir) - val src_path = Path.explode(file) - val node = File.symbolic_path(master_dir + src_path) - Command.Blob.read_file(Document.Node.Name(node), src_path) - }).user_error - } - Command.Blobs_Info(blobs) - case None => Command.Blobs_Info.none - } - } + override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = + Command.Blobs_Info.make(session_blobs(node_name)) + + override def build_blobs(node_name: Document.Node.Name): Document.Blobs = + Document.Blobs.make(session_blobs(node_name)) } object Build_Session_Errors { @@ -418,7 +428,8 @@ cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))), compress = false) - for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { + for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) { + val xml = snapshot.switch(blob_name).xml_markup() export_(Export.MARKUP + (i + 1), xml) } export_(Export.MARKUP, snapshot.xml_markup()) diff -r 711cef61c0ce -r 5e033f907bcc src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Pure/Tools/update.scala Mon Jan 09 17:16:22 2023 +0000 @@ -8,20 +8,59 @@ object Update { - def update(options: Options, logic: String, + def update(options: Options, + update_options: List[Options.Spec], + selection: Sessions.Selection = Sessions.Selection.empty, + base_logics: List[String] = Nil, progress: Progress = new Progress, - log: Logger = No_Logger, + build_heap: Boolean = false, + clean_build: Boolean = false, 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) + numa_shuffling: Boolean = false, + max_jobs: Int = 1, + fresh_build: Boolean = false, + no_build: Boolean = false, + verbose: Boolean = false + ): 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) + // test + options ++ update_options + + def augment_options(name: String): List[Options.Spec] = + if (exclude(name)) Nil else update_options + + + /* build */ - val path_cartouches = context.options.bool("update_path_cartouches") + val build_results = + 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, verbose = verbose, augment_options = augment_options) + + 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 +76,46 @@ 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 build_results(session).ok && !exclude(session) + } { + progress.echo("Session " + session + " ...") + 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_Job.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 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 } @@ -66,13 +126,20 @@ { 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 logic = Dump.default_logic + var max_jobs = 1 + 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 @@ -85,26 +152,37 @@ -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 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 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 - Update theory sources based on PIDE markup. + 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:" -> (arg => logic = arg), + "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 = Value.Int.parse(arg)), + "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))) @@ -112,19 +190,30 @@ 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, 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, + clean_build, + dirs = dirs, + select_dirs = select_dirs, + numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling), + max_jobs = max_jobs, + fresh_build, + no_build = no_build, + verbose = verbose) + } + + sys.exit(results.rc) }) } diff -r 711cef61c0ce -r 5e033f907bcc src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/vscode_model.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Tools/VSCode/src/vscode_model.scala Mon Jan 09 17:16:22 2023 +0000 @@ -142,9 +142,9 @@ /* blob */ - def get_blob: Option[Document.Blob] = + def get_blob: Option[Document.Blobs.Item] = if (is_theory) None - else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) + else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) /* data */ diff -r 711cef61c0ce -r 5e033f907bcc src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Tools/jEdit/src/document_model.scala Mon Jan 09 17:16:22 2023 +0000 @@ -433,9 +433,9 @@ Line.Node_Position(node_name.node, Line.Position.zero.advance(content.text.substring(0, offset))) - def get_blob: Option[Document.Blob] = + def get_blob: Option[Document.Blobs.Item] = if (is_theory) None - else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) + else Some(Document.Blobs.Item(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) def untyped_data: AnyRef = content.data @@ -575,7 +575,7 @@ def reset_blob(): Unit = GUI_Thread.require { blob = None } - def get_blob: Option[Document.Blob] = GUI_Thread.require { + def get_blob: Option[Document.Blobs.Item] = GUI_Thread.require { if (is_theory) None else { val (bytes, text, chunk) = @@ -588,7 +588,7 @@ x } val changed = !is_stable - Some(Document.Blob(bytes, text, chunk, changed)) + Some(Document.Blobs.Item(bytes, text, chunk, changed)) } } @@ -617,7 +617,7 @@ def node_required: Boolean = buffer_state.get_node_required def set_node_required(b: Boolean): Unit = buffer_state.set_node_required(b) - def get_blob: Option[Document.Blob] = buffer_state.get_blob + def get_blob: Option[Document.Blobs.Item] = buffer_state.get_blob def untyped_data: AnyRef = buffer_state.untyped_data diff -r 711cef61c0ce -r 5e033f907bcc src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Mon Jan 09 17:16:04 2023 +0000 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Jan 09 17:16:22 2023 +0000 @@ -31,7 +31,7 @@ results: Command.Results = Command.Results.empty ): (String, JEdit_Rendering) = { val command = Command.rich_text(Document_ID.make(), results, formatted_body) - val snippet = snapshot.snippet(command) + val snippet = snapshot.snippet(command, Document.Blobs.empty) val model = File_Model.init(PIDE.session) val rendering = apply(snippet, model, PIDE.options.value) (command.source, rendering)