--- 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.
--- 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>\<open>export_generated_files\<close> 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 \<open>build.props\<close>} file is expected directly in the toplevel
+ directory, instead of @{path \<open>etc/build.props\<close>} 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
--- 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>\<open>-f\<close> forces a fresh build of all selected sessions and their
requirements.
- \<^medskip>
- Option \<^verbatim>\<open>-n\<close> 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>\<open>-n\<close> 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>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
@@ -774,8 +774,8 @@
text \<open>
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]
\<open>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.\<close>}
+ Update theory sources based on PIDE markup produced by "isabelle build".\<close>}
- \<^medskip> Options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> 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>\<open>-b\<close> 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>\<open>-l\<close> specifies one or more base logics: these sessions and their
+ ancestors are \<^emph>\<open>excluded\<close> from the update.
- \<^medskip> Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity.
-
- \<^medskip> Option \<^verbatim>\<open>-o\<close> overrides Isabelle system options as for @{tool build}
- (\secref{sec:tool-build}). Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close>
- options, by relying on naming convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for
- ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
+ \<^medskip> Option \<^verbatim>\<open>-u\<close> refers to specific \<^verbatim>\<open>update\<close> options, by relying on naming
+ convention: ``\<^verbatim>\<open>-u\<close>~\<open>OPT\<close>'' is a shortcut for ``\<^verbatim>\<open>-o\<close>~\<^verbatim>\<open>update_\<close>\<open>OPT\<close>''.
\<^medskip> The following \<^verbatim>\<open>update\<close> options are supported:
@@ -850,20 +848,14 @@
@{verbatim [display] \<open> isabelle update -u mixfix_cartouches HOL-Analysis\<close>}
- \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close> ---
- using its image as starting point (for reduced resource requirements):
-
- @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -b HOL-Analysis -B HOL-Analysis\<close>}
+ \<^smallskip> Update the same for all application sessions based on \<^verbatim>\<open>HOL-Analysis\<close>, but
+ do not change the underlying \<^verbatim>\<open>HOL\<close> (and \<^verbatim>\<open>Pure\<close>) session:
- \<^smallskip> Update sessions that build on \<^verbatim>\<open>HOL-Proofs\<close>, which need to be run
- separately with special options as follows:
+ @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -l HOL -B HOL-Analysis\<close>}
- @{verbatim [display] \<open> isabelle update -u mixfix_cartouches -l HOL-Proofs -B HOL-Proofs
- -o record_proofs=2\<close>}
+ \<^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] \<open> isabelle update -u mixfix_cartouches -n -a\<close>}
\<close>
--- 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 \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>a\<in>s. dist x a = dist y a)"
by auto
-ML_file "metric_arith.ML"
+ML_file \<open>metric_arith.ML\<close>
method_setup metric = \<open>
Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
--- 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 \<open>Tools/BNF/bnf_lift.ML\<close>
hide_fact
sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit
--- 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()
}
--- 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
--- 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)
}
}
--- 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 =
--- 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()
--- 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\<close>
-external_file "ROOT0.ML"
-external_file "ROOT.ML"
+external_file \<open>ROOT0.ML\<close>
+external_file \<open>ROOT.ML\<close>
subsection \<open>Embedded ML text\<close>
--- 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";
+
--- 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))
--- 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))
--- 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 {
--- 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)
}
--- 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 =
--- 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
--- 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())
--- 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)
})
}
--- 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 */
--- 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
--- 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)