--- a/etc/build.props Sun Jan 01 12:24:00 2023 +0000
+++ b/etc/build.props Sun Jan 01 22:01:53 2023 +0100
@@ -315,7 +315,7 @@
isabelle.Scala$Handler \
isabelle.Scala_Functions \
isabelle.Server_Commands \
- isabelle.Sessions$File_Format \
+ isabelle.Sessions$ROOTS_File_Format \
isabelle.Simplifier_Trace$Handler \
isabelle.Tools \
isabelle.jedit.JEdit_Plugin0 \
--- a/src/Pure/General/graph.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/General/graph.scala Sun Jan 01 22:01:53 2023 +0100
@@ -27,7 +27,7 @@
def make[Key, A](
entries: List[((Key, A), List[Key])],
- symmetric: Boolean = false)(
+ converse: Boolean = false)(
implicit ord: Ordering[Key]
): Graph[Key, A] = {
val graph1 =
@@ -38,7 +38,7 @@
entries.foldLeft(graph1) {
case (graph, ((x, _), ys)) =>
ys.foldLeft(graph) {
- case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y)
+ case (g, y) => if (converse) g.add_edge(y, x) else g.add_edge(x, y)
}
}
graph2
--- a/src/Pure/General/url.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/General/url.scala Sun Jan 01 22:01:53 2023 +0100
@@ -102,7 +102,7 @@
def canonical_file_name(uri: String): String = canonical_file(uri).getPath
- /* generic path notation: local, ssh, rsync, ftp, http */
+ /* generic path notation: standard, platform, ssh, rsync, ftp, http */
private val separators1 = "/\\"
private val separators2 = ":/\\"
--- a/src/Pure/PIDE/document.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/document.scala Sun Jan 01 22:01:53 2023 +0100
@@ -94,6 +94,9 @@
def apply(node: String, master_dir: String = "", theory: String = ""): Name =
new Name(node, master_dir, theory)
+ def loaded_theory(theory: String): Document.Node.Name =
+ Name(theory, theory = theory)
+
val empty: Name = Name("")
object Ordering extends scala.math.Ordering[Name] {
@@ -103,7 +106,7 @@
type Graph[A] = isabelle.Graph[Node.Name, A]
def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] =
- Graph.make(entries, symmetric = true)(Ordering)
+ Graph.make(entries, converse = true)(Ordering)
}
final class Name private(val node: String, val master_dir: String, val theory: String) {
@@ -125,16 +128,11 @@
override def toString: String = if (is_theory) theory else node
- def map(f: String => String): Name =
- new Name(f(node), f(master_dir), theory)
-
def json: JSON.Object.T =
JSON.Object("node_name" -> node, "theory_name" -> theory)
}
sealed case class Entry(name: Node.Name, header: Node.Header) {
- def map(f: String => String): Entry = copy(name = name.map(f))
-
override def toString: String = name.toString
}
--- a/src/Pure/PIDE/protocol.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/protocol.scala Sun Jan 01 22:01:53 2023 +0100
@@ -28,7 +28,7 @@
case (Markup.Name(name), Position.File(file), Position.Id(id))
if Path.is_wellformed(file) =>
val master_dir = Path.explode(file).dir.implode
- Some((Document.Node.Name(file, master_dir, name), id))
+ Some((Document.Node.Name(file, master_dir = master_dir, theory = name), id))
case _ => None
}
}
--- a/src/Pure/PIDE/resources.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/resources.scala Sun Jan 01 22:01:53 2023 +0100
@@ -78,12 +78,9 @@
def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
val node = append(dir, file)
val master_dir = append(dir, file.dir)
- Document.Node.Name(node, master_dir, theory)
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
- def loaded_theory_node(theory: String): Document.Node.Name =
- Document.Node.Name(theory, "", theory)
-
/* source files of Isabelle/ML bootstrap */
@@ -141,7 +138,7 @@
for {
(name, theory) <- Thy_Header.ml_roots
path = (pure_dir + Path.explode(name)).expand
- node_name = Document.Node.Name(path.implode, path.dir.implode, theory)
+ node_name = Document.Node.Name(path.implode, master_dir = path.dir.implode, theory = theory)
file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)())
} yield file
}
@@ -175,12 +172,12 @@
if (literal_import && !Url.is_base_name(s)) {
error("Bad import of theory from other session via file-path: " + quote(s))
}
- if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+ if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else {
find_theory_node(theory) match {
case Some(node_name) => node_name
case None =>
- if (Url.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
+ if (Url.is_base_name(s) && literal_theory(s)) Document.Node.Name.loaded_theory(theory)
else file_node(Path.explode(s).thy, dir = dir, theory = theory)
}
}
--- a/src/Pure/PIDE/session.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/PIDE/session.scala Sun Jan 01 22:01:53 2023 +0100
@@ -487,7 +487,7 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
val id = Value.Long.unapply(args.id.get).get
- val entry = Export.make_entry(Sessions.DRAFT, args, msg.chunk, cache)
+ val entry = Export.Entry.make(Sessions.DRAFT, args, msg.chunk, cache)
change_command(_.add_export(id, (args.serial, entry)))
case Protocol.Loading_Theory(node_name, id) =>
@@ -563,7 +563,7 @@
val snapshot = global_state.change_result(_.end_theory(id))
finished_theories.post(snapshot)
}
- file_formats.stop_session
+ file_formats.stop_session()
phase = Session.Terminated(result)
prover.reset()
--- a/src/Pure/ROOT.ML Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/ROOT.ML Sun Jan 01 22:01:53 2023 +0100
@@ -366,4 +366,3 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
-
--- a/src/Pure/Thy/bibtex.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/bibtex.scala Sun Jan 01 22:01:53 2023 +0100
@@ -28,6 +28,7 @@
override def theory_content(name: String): String =
"""theory "bib" imports Pure begin bibtex_file """ +
Outer_Syntax.quote_string(name) + """ end"""
+ override def theory_excluded(name: String): Boolean = name == "bib"
override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
val name = snapshot.node_name
--- a/src/Pure/Thy/export.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/export.scala Sun Jan 01 22:01:53 2023 +0100
@@ -107,13 +107,36 @@
def message(msg: String, theory_name: String, name: String): String =
msg + " " + quote(name) + " for theory " + quote(theory_name)
- def empty_entry(theory_name: String, name: String): Entry =
- Entry(Entry_Name(theory = theory_name, name = name),
- false, Future.value(false, Bytes.empty), XML.Cache.none)
+ object Entry {
+ def apply(
+ entry_name: Entry_Name,
+ executable: Boolean,
+ body: Future[(Boolean, Bytes)],
+ cache: XML.Cache
+ ): Entry = new Entry(entry_name, executable, body, cache)
+
+ def empty(theory_name: String, name: String): Entry =
+ Entry(Entry_Name(theory = theory_name, name = name),
+ false, Future.value(false, Bytes.empty), XML.Cache.none)
- sealed case class Entry(
- entry_name: Entry_Name,
- executable: Boolean,
+ def make(
+ session_name: String,
+ args: Protocol.Export.Args,
+ bytes: Bytes,
+ cache: XML.Cache
+ ): Entry = {
+ val body =
+ if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
+ else Future.value((false, bytes))
+ val entry_name =
+ Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
+ Entry(entry_name, args.executable, body, cache)
+ }
+ }
+
+ final class Entry private(
+ val entry_name: Entry_Name,
+ val executable: Boolean,
body: Future[(Boolean, Bytes)],
cache: XML.Cache
) {
@@ -122,6 +145,9 @@
def name: String = entry_name.name
override def toString: String = name
+ def is_finished: Boolean = body.is_finished
+ def cancel(): Unit = body.cancel()
+
def compound_name: String = entry_name.compound_name
def name_has_prefix(s: String): Boolean = name.startsWith(s)
@@ -130,25 +156,24 @@
def name_extends(elems: List[String]): Boolean =
name_elems.startsWith(elems) && name_elems != elems
- def text: String = uncompressed.text
-
- def uncompressed: Bytes = {
- val (compressed, bytes) = body.join
- if (compressed) bytes.uncompress(cache = cache.compress) else bytes
+ def bytes: Bytes = {
+ val (compressed, bs) = body.join
+ if (compressed) bs.uncompress(cache = cache.compress) else bs
}
- def uncompressed_yxml: XML.Body =
- YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
+ def text: String = bytes.text
+
+ def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache)
def write(db: SQL.Database): Unit = {
- val (compressed, bytes) = body.join
+ val (compressed, bs) = body.join
db.using_statement(Data.table.insert()) { stmt =>
stmt.string(1) = session_name
stmt.string(2) = theory_name
stmt.string(3) = name
stmt.bool(4) = executable
stmt.bool(5) = compressed
- stmt.bytes(6) = bytes
+ stmt.bytes(6) = bs
stmt.execute()
}
}
@@ -176,19 +201,6 @@
(entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name))
}
- def make_entry(
- session_name: String,
- args: Protocol.Export.Args,
- bytes: Bytes,
- cache: XML.Cache
- ): Entry = {
- val body =
- if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
- else Future.value((false, bytes))
- val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
- Entry(entry_name, args.executable, body, cache)
- }
-
/* database consumer thread */
@@ -200,7 +212,7 @@
private val consumer =
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
- bulk = { case (entry, _) => entry.body.is_finished },
+ bulk = { case (entry, _) => entry.is_finished },
consume =
{ (args: List[(Entry, Boolean)]) =>
val results =
@@ -208,7 +220,7 @@
for ((entry, strict) <- args)
yield {
if (progress.stopped) {
- entry.body.cancel()
+ entry.cancel()
Exn.Res(())
}
else if (entry.entry_name.readable(db)) {
@@ -227,7 +239,7 @@
def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
if (!progress.stopped && !body.is_empty) {
val args = if (db.is_server) args0.copy(compress = false) else args0
- consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
+ consumer.send(Entry.make(session_name, args, body, cache) -> args.strict)
}
}
@@ -403,7 +415,7 @@
def apply(theory: String, name: String, permissive: Boolean = false): Entry =
get(theory, name) match {
- case None if permissive => empty_entry(theory, name)
+ case None if permissive => Entry.empty(theory, name)
case None => error("Missing export entry " + quote(compound_name(theory, name)))
case Some(entry) => entry
}
@@ -411,6 +423,20 @@
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 db_source: Option[String] =
+ db_hierarchy.view.map(database =>
+ database_context.store.read_sources(database.db, database.session, name.node))
+ .collectFirst({ case Some(bytes) => bytes.text })
+ snapshot_source orElse db_source getOrElse ""
+ }
+
def classpath(): List[File.Content] = {
(for {
session <- session_stack.iterator
@@ -420,7 +446,7 @@
entry_name <- entry_names(session = session).iterator
if matcher(entry_name)
entry <- get(entry_name.theory, entry_name.name).iterator
- } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
+ } yield File.content(entry.entry_name.make_path(), entry.bytes)).toList
}
override def toString: String =
@@ -438,9 +464,9 @@
def apply(name: String, permissive: Boolean = false): Entry =
session_context.apply(theory, name, permissive = permissive)
- def uncompressed_yxml(name: String): XML.Body =
+ def yxml(name: String): XML.Body =
get(name) match {
- case Some(entry) => entry.uncompressed_yxml
+ case Some(entry) => entry.yxml
case None => Nil
}
@@ -492,7 +518,7 @@
val path = export_dir + entry_name.make_path(prune = export_prune)
progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
Isabelle_System.make_directory(path.dir)
- val bytes = entry.uncompressed
+ val bytes = entry.bytes
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
File.set_executable(path, entry.executable)
}
--- a/src/Pure/Thy/export_theory.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/export_theory.scala Sun Jan 01 22:01:53 2023 +0100
@@ -103,7 +103,7 @@
def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
theory_context.get(Export.THEORY_PREFIX + "parents")
- .map(entry => Library.trim_split_lines(entry.uncompressed.text))
+ .map(entry => Library.trim_split_lines(entry.text))
def theory_names(
session_context: Export.Session_Context,
@@ -233,7 +233,7 @@
case _ => err()
}
}
- theory_context.uncompressed_yxml(export_name).map(decode_entity)
+ theory_context.yxml(export_name).map(decode_entity)
}
@@ -393,7 +393,7 @@
for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
yield {
- val body = entry.uncompressed_yxml
+ val body = entry.yxml
val (typargs, (args, (prop_body, proof_body))) = {
import XML.Decode._
import Term_XML.Decode._
@@ -539,7 +539,7 @@
}
def read_classrel(theory_context: Export.Theory_Context): List[Classrel] = {
- val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
+ val body = theory_context.yxml(Export.THEORY_PREFIX + "classrel")
val classrel = {
import XML.Decode._
list(pair(decode_prop, pair(string, string)))(body)
@@ -559,7 +559,7 @@
}
def read_arities(theory_context: Export.Theory_Context): List[Arity] = {
- val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
+ val body = theory_context.yxml(Export.THEORY_PREFIX + "arities")
val arities = {
import XML.Decode._
import Term_XML.Decode._
@@ -577,7 +577,7 @@
}
def read_constdefs(theory_context: Export.Theory_Context): List[Constdef] = {
- val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
+ val body = theory_context.yxml(Export.THEORY_PREFIX + "constdefs")
val constdefs = {
import XML.Decode._
list(pair(string, string))(body)
@@ -606,7 +606,7 @@
}
def read_typedefs(theory_context: Export.Theory_Context): List[Typedef] = {
- val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
+ val body = theory_context.yxml(Export.THEORY_PREFIX + "typedefs")
val typedefs = {
import XML.Decode._
import Term_XML.Decode._
@@ -640,7 +640,7 @@
}
def read_datatypes(theory_context: Export.Theory_Context): List[Datatype] = {
- val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
+ val body = theory_context.yxml(Export.THEORY_PREFIX + "datatypes")
val datatypes = {
import XML.Decode._
import Term_XML.Decode._
@@ -730,7 +730,7 @@
}
def read_spec_rules(theory_context: Export.Theory_Context): List[Spec_Rule] = {
- val body = theory_context.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
+ val body = theory_context.yxml(Export.THEORY_PREFIX + "spec_rules")
val spec_rules = {
import XML.Decode._
import Term_XML.Decode._
@@ -753,7 +753,7 @@
def read_others(theory_context: Export.Theory_Context): Map[String, List[Entity[Other]]] = {
val kinds =
theory_context.get(Export.THEORY_PREFIX + "other_kinds") match {
- case Some(entry) => split_lines(entry.uncompressed.text)
+ case Some(entry) => split_lines(entry.text)
case None => Nil
}
val other = Other()
--- a/src/Pure/Thy/file_format.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/file_format.scala Sun Jan 01 22:01:53 2023 +0100
@@ -28,6 +28,8 @@
def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
+ def theory_excluded(name: String): Boolean = file_formats.exists(_.theory_excluded(name))
+
def parse_data(name: String, text: String): AnyRef =
get(name) match {
case Some(file_format) => file_format.parse_data(name, text)
@@ -49,7 +51,7 @@
def prover_options(options: Options): Options =
agents.foldLeft(options) { case (opts, agent) => agent.prover_options(opts) }
- def stop_session: Unit = agents.foreach(_.stop())
+ def stop_session(): Unit = agents.foreach(_.stop())
}
trait Agent {
@@ -74,18 +76,19 @@
def theory_suffix: String = ""
def theory_content(name: String): String = ""
+ def theory_excluded(name: String): Boolean = false
def make_theory_name(
resources: Resources,
name: Document.Node.Name
): Option[Document.Node.Name] = {
for {
- thy <- Url.get_base_name(name.node)
+ theory <- Url.get_base_name(name.node)
if detect(name.node) && theory_suffix.nonEmpty
}
yield {
- val thy_node = resources.append(name.node, Path.explode(theory_suffix))
- Document.Node.Name(thy_node, name.master_dir, thy)
+ val node = resources.append(name.node, Path.explode(theory_suffix))
+ Document.Node.Name(node, master_dir = name.master_dir, theory = theory)
}
}
--- a/src/Pure/Thy/sessions.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/sessions.scala Sun Jan 01 22:01:53 2023 +0100
@@ -32,12 +32,13 @@
def is_pure(name: String): Boolean = name == Thy_Header.PURE
def illegal_session(name: String): Boolean = name == "" || name == DRAFT
- def illegal_theory(name: String): Boolean = name == root_name || name == "bib"
+ def illegal_theory(name: String): Boolean =
+ name == root_name || File_Format.registry.theory_excluded(name)
/* ROOTS file format */
- class File_Format extends isabelle.File_Format {
+ class ROOTS_File_Format extends File_Format {
val format_name: String = roots_name
val file_ext = ""
@@ -51,6 +52,7 @@
override def theory_content(name: String): String =
"""theory "ROOTS" imports Pure begin ROOTS_file """ +
Outer_Syntax.quote_string(name) + """ end"""
+ override def theory_excluded(name: String): Boolean = name == "ROOTS"
}
@@ -247,7 +249,7 @@
var cache_sources = Map.empty[JFile, SHA1.Digest]
def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = {
for {
- path <- paths
+ path <- Library.distinct(paths)
file = path.file
if cache_sources.isDefinedAt(file) || file.isFile
}
@@ -1335,6 +1337,21 @@
" ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
}
+ object Sources {
+ val session_name = SQL.Column.string("session_name").make_primary_key
+ val name = SQL.Column.string("name").make_primary_key
+ val digest = SQL.Column.string("digest")
+ val compressed = SQL.Column.bool("compressed")
+ val body = SQL.Column.bytes("body")
+
+ val table =
+ SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body))
+
+ def where_equal(session_name: String, name: String = ""): SQL.Source =
+ "WHERE " + Sources.session_name.equal(session_name) +
+ (if (name == "") "" else " AND " + Sources.name.equal(name))
+ }
+
def store(options: Options, cache: Term.Cache = Term.Cache.make()): Store =
new Store(options, cache)
@@ -1493,6 +1510,9 @@
db.using_statement(Session_Info.augment_table)(_.execute())
}
+ db.create_table(Sources.table)
+ db.using_statement(Sources.table.delete(Sources.where_equal(name)))(_.execute())
+
db.create_table(Export.Data.table)
db.using_statement(
Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute())
@@ -1519,14 +1539,33 @@
def write_session_info(
db: SQL.Database,
- name: String,
+ session_base: Base,
build_log: Build_Log.Session_Info,
build: Build.Session_Info
): Unit = {
+ val sources =
+ for ((path, digest) <- session_base.session_sources) yield {
+ val bytes = Bytes.read(path)
+ if (bytes.sha1_digest != digest) error("Erratic change of file content: " + path)
+ val name = path.implode_symbolic
+ val (compressed, body) =
+ bytes.maybe_compress(Compress.Options_Zstd(), cache = cache.compress)
+ (name, digest, compressed, body)
+ }
+
db.transaction {
- val table = Session_Info.table
- db.using_statement(table.insert()) { stmt =>
- stmt.string(1) = name
+ for ((name, digest, compressed, body) <- sources) {
+ db.using_statement(Sources.table.insert()) { stmt =>
+ stmt.string(1) = session_base.session_name
+ stmt.string(2) = name
+ stmt.string(3) = digest.toString
+ stmt.bool(4) = compressed
+ stmt.bytes(5) = body
+ stmt.execute()
+ }
+ }
+ db.using_statement(Session_Info.table.insert()) { stmt =>
+ stmt.string(1) = session_base.session_name
stmt.bytes(2) = Properties.encode(build_log.session_timing)
stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
@@ -1586,5 +1625,20 @@
}
else None
}
+
+ def read_sources(db: SQL.Database, session_name: String, name: String): Option[Bytes] = {
+ val sql =
+ Sources.table.select(List(Sources.compressed, Sources.body),
+ Sources.where_equal(session_name, name = name))
+ db.using_statement(sql) { stmt =>
+ val res = stmt.execute_query()
+ if (!res.next()) None
+ else {
+ val compressed = res.bool(Sources.compressed)
+ val bs = res.bytes(Sources.body)
+ Some(if (compressed) bs.uncompress(cache = cache.compress) else bs)
+ }
+ }
+ }
}
}
--- a/src/Pure/Thy/thy_header.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Thy/thy_header.scala Sun Jan 01 22:01:53 2023 +0100
@@ -93,7 +93,8 @@
def theory_name(s: String): String =
get_thy_name(s) match {
- case Some(name) => bootstrap_name(name)
+ case Some(name) =>
+ bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
case None =>
Url.get_base_name(s) match {
case Some(name) =>
@@ -109,9 +110,6 @@
def is_bootstrap(theory: String): Boolean =
bootstrap_thys.exists({ case (_, b) => b == theory })
- def bootstrap_name(theory: String): String =
- bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
-
/* parser */
--- a/src/Pure/Tools/build.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/build.scala Sun Jan 01 22:01:53 2023 +0100
@@ -348,7 +348,7 @@
// write database
using(store.open_database(session_name, output = true))(db =>
- store.write_session_info(db, session_name,
+ store.write_session_info(db, build_deps(session_name),
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
--- a/src/Pure/Tools/build_job.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/build_job.scala Sun Jan 01 22:01:53 2023 +0100
@@ -22,7 +22,7 @@
def read_xml(name: String): XML.Body =
YXML.parse_body(
- Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)),
+ Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)),
cache = theory_context.cache)
for {
@@ -274,8 +274,8 @@
override val cache: Term.Cache = store.cache
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
- val name1 = name.map(s => Path.explode(s).expand.implode)
- session_background.base.load_commands.get(name1) match {
+ val expand_node = Document.Node.Name(Path.explode(name.node).expand.implode)
+ session_background.base.load_commands.get(expand_node) match {
case Some(spans) =>
val syntax = session_background.base.theory_syntax(name)
Command.build_blobs_info(syntax, name, spans)
--- a/src/Pure/Tools/dump.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/dump.scala Sun Jan 01 22:01:53 2023 +0100
@@ -57,13 +57,13 @@
for {
entry <- args.snapshot.exports
if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
- } args.write(Path.explode(entry.name), entry.uncompressed)),
+ } args.write(Path.explode(entry.name), entry.bytes)),
Aspect("theory", "foundational theory content",
args =>
for {
entry <- args.snapshot.exports
if entry.name_has_prefix(Export.THEORY_PREFIX)
- } args.write(Path.explode(entry.name), entry.uncompressed),
+ } args.write(Path.explode(entry.name), entry.bytes),
options = List("export_theory"))
).sortBy(_.name)
--- a/src/Pure/Tools/server_commands.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Pure/Tools/server_commands.scala Sun Jan 01 22:01:53 2023 +0100
@@ -266,7 +266,7 @@
val matcher = Export.make_matcher(List(args.export_pattern))
for { entry <- snapshot.exports if matcher(entry.entry_name) }
yield {
- val (base64, body) = entry.uncompressed.maybe_encode_base64
+ val (base64, body) = entry.bytes.maybe_encode_base64
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body)
}
}))
--- a/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 01 22:01:53 2023 +0100
@@ -93,10 +93,10 @@
find_theory(file) getOrElse {
val node = file.getPath
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
- if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+ if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else {
val master_dir = file.getParent
- Document.Node.Name(node, master_dir, theory)
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
}
--- a/src/Tools/jEdit/src/isabelle_export.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Tools/jEdit/src/isabelle_export.scala Sun Jan 01 22:01:53 2023 +0100
@@ -56,7 +56,7 @@
} yield {
val is_dir = entry.name_elems.length > depth
val path = Export.implode_name(theory :: entry.name_elems.take(depth))
- val file_size = if (is_dir) None else Some(entry.uncompressed.length.toLong)
+ val file_size = if (is_dir) None else Some(entry.bytes.length.toLong)
(path, file_size)
}).toSet.toList
(for ((path, file_size) <- entries.iterator) yield {
@@ -86,7 +86,7 @@
if node_name.theory == theory
(_, entry) <- snapshot.state.node_exports(version, node_name).iterator
if entry.name_elems == name_elems
- } yield entry.uncompressed).find(_ => true).getOrElse(Bytes.empty)
+ } yield entry.bytes).find(_ => true).getOrElse(Bytes.empty)
bytes.stream()
}
--- a/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 01 12:24:00 2023 +0000
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 01 22:01:53 2023 +0100
@@ -35,10 +35,10 @@
val vfs = VFSManager.getVFSForPath(path)
val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
- if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
+ if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
else {
val master_dir = vfs.getParentOfPath(path)
- Document.Node.Name(node, master_dir, theory)
+ Document.Node.Name(node, master_dir = master_dir, theory = theory)
}
}