# HG changeset patch # User wenzelm # Date 1636664068 -3600 # Node ID 510296c0d8d17f468435b0f41248cc0d5dbbb1fc # Parent eaeab1358ced2d163e77fe56fc6ba783e77117d3 clarified signature: avoid potential misunderstanding of Resources.empty as proper Resources; diff -r eaeab1358ced -r 510296c0d8d1 src/Pure/PIDE/resources.scala --- 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( diff -r eaeab1358ced -r 510296c0d8d1 src/Pure/Thy/presentation.scala --- 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) diff -r eaeab1358ced -r 510296c0d8d1 src/Pure/Tools/build.scala --- 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) }) diff -r eaeab1358ced -r 510296c0d8d1 src/Pure/Tools/build_job.scala --- 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) => diff -r eaeab1358ced -r 510296c0d8d1 src/Pure/Tools/profiling_report.scala --- 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