--- a/src/Pure/Admin/build_scala.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/Admin/build_scala.scala Sat Dec 17 21:26:36 2022 +0100
@@ -78,7 +78,7 @@
download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
File.write(component_dir.LICENSE,
- Url.read(Url("https://www.apache.org/licenses/LICENSE-2.0.txt")))
+ Url.read("https://www.apache.org/licenses/LICENSE-2.0.txt"))
/* classpath */
--- a/src/Pure/ML_Bootstrap.thy Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/ML_Bootstrap.thy Sat Dec 17 21:26:36 2022 +0100
@@ -8,8 +8,6 @@
imports Pure
begin
-external_file "$POLYML_EXE"
-
ML \<open>
#allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
if member (op =) ML_Name_Space.hidden_structures name then
--- a/src/Pure/PIDE/command.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/PIDE/command.scala Sat Dec 17 21:26:36 2022 +0100
@@ -464,7 +464,7 @@
loaded_files.files.map(file =>
(Exn.capture {
val src_path = Path.explode(file)
- val name = Document.Node.Name(resources.append(node_name, src_path))
+ val name = Document.Node.Name(resources.append(node_name.master_dir, src_path))
val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
Blob(name, src_path, content)
}).user_error)
--- a/src/Pure/PIDE/document.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/PIDE/document.scala Sat Dec 17 21:26:36 2022 +0100
@@ -91,6 +91,9 @@
def bad_header(msg: String): Header = Header(errors = List(msg))
object Name {
+ def apply(node: String, master_dir: String = "", theory: String = ""): Name =
+ new Name(node, master_dir, theory)
+
val empty: Name = Name("")
object Ordering extends scala.math.Ordering[Name] {
@@ -103,7 +106,7 @@
Graph.make(entries, symmetric = true)(Ordering)
}
- sealed case class Name(node: String, master_dir: String = "", theory: String = "") {
+ final class Name private(val node: String, val master_dir: String, val theory: String) {
override def hashCode: Int = node.hashCode
override def equals(that: Any): Boolean =
that match {
@@ -114,17 +117,14 @@
def path: Path = Path.explode(File.standard_path(node))
def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
- def expand: Name =
- Name(path.expand.implode, master_dir_path.expand.implode, theory)
-
def is_theory: Boolean = theory.nonEmpty
def theory_base_name: String = Long_Name.base_name(theory)
override def toString: String = if (is_theory) theory else node
- def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
- def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
+ 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)
--- a/src/Pure/PIDE/headless.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/PIDE/headless.scala Sat Dec 17 21:26:36 2022 +0100
@@ -602,14 +602,12 @@
}
class Resources private[Headless](
- val options: Options,
- session_background: Sessions.Background,
- log: Logger = No_Logger)
- extends isabelle.Resources(session_background, log = log) {
+ val options: Options,
+ session_background: Sessions.Background,
+ log: Logger = No_Logger)
+ extends isabelle.Resources(session_background.check_errors, log = log) {
resources =>
- session_background.check_errors
-
val store: Sessions.Store = Sessions.store(options)
--- a/src/Pure/PIDE/rendering.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Dec 17 21:26:36 2022 +0100
@@ -348,7 +348,7 @@
if (text == "" || text.endsWith("/")) (path, "")
else (path.dir, path.file_name)
- val directory = new JFile(session.resources.append(snapshot.node_name, dir))
+ val directory = new JFile(session.resources.append(snapshot.node_name.master_dir, dir))
val files = directory.listFiles
if (files == null) Nil
else {
@@ -616,7 +616,8 @@
}
def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
- if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
+ if (Path.is_valid(name)) session.resources.append(node_name.master_dir, Path.explode(name))
+ else name
def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] = {
val results =
--- a/src/Pure/PIDE/resources.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Dec 17 21:26:36 2022 +0100
@@ -31,9 +31,8 @@
def sessions_structure: Sessions.Structure = session_background.sessions_structure
def session_base: Sessions.Base = session_background.base
- def session_errors: List[String] = session_background.errors
- override def toString: String = "Resources(" + session_base.toString + ")"
+ override def toString: String = "Resources(" + session_base.print_body + ")"
/* init session */
@@ -74,9 +73,6 @@
def append(dir: String, source_path: Path): String =
(Path.explode(dir) + source_path).expand.implode
- def append(node_name: Document.Node.Name, source_path: Path): String =
- append(node_name.master_dir, source_path)
-
def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
val node = append(dir, file)
val master_dir = append(dir, file.dir)
--- a/src/Pure/Thy/sessions.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Dec 17 21:26:36 2022 +0100
@@ -78,10 +78,11 @@
) {
def session_entry: (String, Base) = session_name -> this
- override def toString: String =
- "Sessions.Base(session_name = " + quote(session_name) +
- ", loaded_theories = " + loaded_theories.size +
- ", used_theories = " + used_theories.length + ")"
+ override def toString: String = "Sessions.Base(" + print_body + ")"
+ def print_body: String =
+ "session_name = " + quote(session_name) +
+ ", loaded_theories = " + loaded_theories.size +
+ ", used_theories = " + used_theories.length
def all_document_theories: List[Document.Node.Name] =
proper_session_theories ::: document_theories
--- a/src/Pure/Tools/build.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/Tools/build.scala Sat Dec 17 21:26:36 2022 +0100
@@ -240,8 +240,6 @@
else deps0
}
- val build_sessions = build_deps.sessions_structure
-
/* check unknown files */
@@ -251,20 +249,18 @@
(_, base) <- build_deps.session_bases.iterator
(path, _) <- base.session_sources.iterator
} yield path).toList
- val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
- val unknown_files =
- Mercurial.check_files(source_files)._2.
- filterNot(path => exclude_files.contains(path.canonical_file))
- if (unknown_files.nonEmpty) {
- progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
- unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
+ Mercurial.check_files(source_files)._2 match {
+ case Nil =>
+ case unknown_files =>
+ progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
+ unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
}
}
/* main build process */
- val queue = Queue(progress, build_sessions, store)
+ val queue = Queue(progress, build_deps.sessions_structure, store)
store.prepare_output_dir()
@@ -380,7 +376,7 @@
pending.dequeue(running.isDefinedAt) match {
case Some((session_name, info)) =>
val ancestor_results =
- build_sessions.build_requirements(List(session_name)).
+ build_deps.sessions_structure.build_requirements(List(session_name)).
filterNot(_ == session_name).map(results(_))
val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
@@ -428,7 +424,7 @@
val numa_node = numa_nodes.next(used_node)
val job =
- new Build_Job(progress, session_name, info, build_deps, store, do_store,
+ new Build_Job(progress, build_deps.background(session_name), store, do_store,
log, session_setup, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
@@ -462,7 +458,7 @@
def presentation_sessions(config: Browser_Info.Config): List[String] =
(for {
- name <- build_sessions.build_topological_order.iterator
+ name <- build_deps.sessions_structure.build_topological_order.iterator
result <- build_results.get(name)
if result.ok && config.enabled(result.info)
} yield name).toList
--- a/src/Pure/Tools/build_job.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Dec 17 21:26:36 2022 +0100
@@ -237,9 +237,7 @@
}
class Build_Job(progress: Progress,
- session_name: String,
- val info: Sessions.Info,
- deps: Sessions.Deps,
+ session_background: Sessions.Background,
store: Sessions.Store,
do_store: Boolean,
log: Logger,
@@ -247,15 +245,13 @@
val numa_node: Option[Int],
command_timings0: List[Properties.T]
) {
+ def session_name: String = session_background.session_name
+ val info: Sessions.Info = session_background.sessions_structure(session_name)
val options: Options = NUMA.policy_options(info.options, numa_node)
- private val session_background = deps.background(session_name)
-
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
val parent = info.parent.getOrElse("")
- val base = deps(parent)
- val result_base = deps(session_name)
val env =
Isabelle_System.settings(
@@ -280,9 +276,10 @@
override val cache: Term.Cache = store.cache
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
- result_base.load_commands.get(name.expand) match {
+ val name1 = name.map(s => Path.explode(s).expand.implode)
+ session_background.base.load_commands.get(name1) match {
case Some(spans) =>
- val syntax = result_base.theory_syntax(name)
+ val syntax = session_background.base.theory_syntax(name)
Command.build_blobs_info(syntax, name, spans)
case None => Command.Blobs_Info.none
}
@@ -488,7 +485,7 @@
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) {
using(Export.open_database_context(store)) { database_context =>
val documents =
- using(database_context.open_session(deps.background(session_name))) {
+ using(database_context.open_session(session_background)) {
session_context =>
Document_Build.build_documents(
Document_Build.context(session_context, progress = progress),
@@ -515,7 +512,7 @@
case _ => None
}).toMap
val used_theory_timings =
- for { (name, _) <- deps(session_name).used_theories }
+ for { (name, _) <- session_background.base.used_theories }
yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
val more_output =
--- a/src/Tools/jEdit/src/jedit_resources.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Dec 17 21:26:36 2022 +0100
@@ -74,7 +74,7 @@
val name = node_name.node
try {
val text =
- if (Url.is_wellformed(name)) Url.read(Url(name))
+ if (Url.is_wellformed(name)) Url.read(name)
else File.read(new JFile(name))
Some(Symbol.decode(Line.normalize(text)))
}
--- a/src/Tools/jEdit/src/main_plugin.scala Sat Dec 17 21:26:24 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Sat Dec 17 21:26:36 2022 +0100
@@ -298,10 +298,12 @@
if (startup_failure.isEmpty) {
message match {
case _: EditorStarted =>
- if (resources.session_errors.nonEmpty) {
- GUI.warning_dialog(jEdit.getActiveView,
- "Bad session structure: may cause problems with theory imports",
- GUI.scrollable_text(cat_lines(resources.session_errors)))
+ try { resources.session_background.check_errors }
+ catch {
+ case ERROR(msg) =>
+ GUI.warning_dialog(jEdit.getActiveView,
+ "Bad session structure: may cause problems with theory imports",
+ GUI.scrollable_text(msg))
}
jEdit.propertiesChanged()