clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources;

--- a/src/Pure/PIDE/resources.scala	Thu Nov 11 13:47:32 2021 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Nov 11 21:54:28 2021 +0100
@@ -16,6 +16,9 @@
 {
   def empty: Resources =
     new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
+
+  def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
+    empty.file_node(file, dir = dir, theory = theory)
 }
 
 class Resources(

--- a/src/Pure/Thy/presentation.scala	Thu Nov 11 13:47:32 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 11 21:54:28 2021 +0100
@@ -99,7 +99,6 @@
     val empty: Entity_Context = new Entity_Context
 
     def make(
-        resources: Resources,
         session: String,
         deps: Sessions.Deps,
         node: Document.Node.Name,
@@ -152,7 +151,7 @@
         {
           (props, props, props, props, props) match {
             case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
-              val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
+              val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
               node_relative(deps, session, node_name).map(html_dir =>
                 HTML.link(html_dir + html_name(node_name), body))
             case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
@@ -163,7 +162,7 @@
                   (if (File.eq(node.path, file_path)) Some(node.theory) else None)
               for {
                 thy_name <- proper_thy_name
-                node_name = resources.file_node(file_path, theory = thy_name)
+                node_name = Resources.file_node(file_path, theory = thy_name)
                 html_dir <- node_relative(deps, session, node_name)
                 html_file = node_file(node_name)
                 html_ref <-
@@ -456,7 +455,6 @@
   }
 
   def session_html(
-    resources: Resources,
     session: String,
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context,
@@ -536,7 +534,7 @@
       }).toMap
 
     def entity_context(name: Document.Node.Name): Entity_Context =
-      Entity_Context.make(resources, session, deps, name, theory_exports)
+      Entity_Context.make(session, deps, name, theory_exports)
 
     val theories: List[XML.Body] =
     {
@@ -558,7 +556,7 @@
       {
         progress.expose_interrupt()
 
-        for (command <- Build_Job.read_theory(db_context, resources, hierarchy, name.theory))
+        for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory))
         yield {
           if (verbose) progress.echo("Presenting theory " + name)
           val snapshot = Document.State.init.snippet(command)

--- a/src/Pure/Tools/build.scala	Thu Nov 11 13:47:32 2021 +0100
+++ b/src/Pure/Tools/build.scala	Thu Nov 11 21:54:28 2021 +0100
@@ -506,7 +506,6 @@
           Presentation.update_chapter(presentation_dir, chapter, entries)
         }
 
-        val resources = Resources.empty
         val html_context = Presentation.html_context(cache = store.cache)
 
         using(store.open_database_context())(db_context =>
@@ -514,7 +513,7 @@
             progress.expose_interrupt()
             progress.echo("Presenting " + info.name + " ...")
             Presentation.session_html(
-              resources, info.name, deps, db_context, progress = progress,
+              info.name, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
               Presentation.elements1, presentation = presentation)
           })

--- a/src/Pure/Tools/build_job.scala	Thu Nov 11 13:47:32 2021 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 11 21:54:28 2021 +0100
@@ -18,7 +18,6 @@
 
   def read_theory(
     db_context: Sessions.Database_Context,
-    resources: Resources,
     session_hierarchy: List[String],
     theory: String,
     unicode_symbols: Boolean = false): Option[Command] =
@@ -33,7 +32,7 @@
 
     (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
       case (Value.Long(id), thy_file :: blobs_files) =>
-        val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
+        val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
 
         val results =
           Command.Results.make(
@@ -44,7 +43,7 @@
           blobs_files.map(file =>
           {
             val path = Path.explode(file)
-            val name = resources.file_node(path)
+            val name = Resources.file_node(path)
             val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
             Command.Blob(name, src_path, None)
           })
@@ -95,8 +94,7 @@
     unicode_symbols: Boolean = false): Unit =
   {
     val store = Sessions.store(options)
-    val resources = Resources.empty
-    val session = new Session(options, resources)
+    val session = new Session(options, Resources.empty)
 
     using(store.open_database_context())(db_context =>
     {
@@ -118,8 +116,7 @@
             if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
           for (thy <- print_theories) {
             val thy_heading = "\nTheory " + quote(thy) + ":"
-            read_theory(db_context, resources, List(session_name), thy,
-              unicode_symbols = unicode_symbols)
+            read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols)
             match {
               case None => progress.echo(thy_heading + " MISSING")
               case Some(command) =>

--- a/src/Pure/Tools/profiling_report.scala	Thu Nov 11 13:47:32 2021 +0100
+++ b/src/Pure/Tools/profiling_report.scala	Thu Nov 11 21:54:28 2021 +0100
@@ -17,7 +17,6 @@
     progress: Progress = new Progress): Unit =
   {
     val store = Sessions.store(options)
-    val resources = Resources.empty
 
     using(store.open_database_context())(db_context =>
     {
@@ -34,7 +33,7 @@
             (for {
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
-              command <- Build_Job.read_theory(db_context, resources, List(session), thy).iterator
+              command <- Build_Job.read_theory(db_context, List(session), thy).iterator
               snapshot = Document.State.init.snippet(command)
               (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList