# HG changeset patch
# User nipkow
# Date 1671308796 -3600
# Node ID 186cf469b95dcaa8f0747ba9026bfdc257607838
# Parent  32c0abd3507164395d20cda8f07dcc2aecc3ada5# Parent  059a68d21f0fee10206ec7f5739db1365341b48d
merged

diff -r 059a68d21f0f -r 186cf469b95d src/Pure/Admin/build_scala.scala
--- 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 */
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/ML_Bootstrap.thy
--- 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
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/PIDE/command.scala
--- 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)
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/PIDE/document.scala
--- 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)
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/PIDE/headless.scala
--- 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)
 
 
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/PIDE/rendering.scala
--- 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 =
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/PIDE/resources.scala
--- 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)
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/Thy/sessions.scala
--- 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
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/Tools/build.scala
--- 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
diff -r 059a68d21f0f -r 186cf469b95d src/Pure/Tools/build_job.scala
--- 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 =
diff -r 059a68d21f0f -r 186cf469b95d src/Tools/jEdit/src/jedit_resources.scala
--- 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)))
       }
diff -r 059a68d21f0f -r 186cf469b95d src/Tools/jEdit/src/main_plugin.scala
--- 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()