# HG changeset patch # User wenzelm # Date 1660740140 -7200 # Node ID 3d8b37b1d798b160447c83806601e02e5da097cf # Parent 648fe09330f38500c6a3ffcb643f05779e19e3bf clarified signature: avoid object-oriented HTML_Context; clarified theory_qualifier --- belongs to the overall Sessions.Structure; diff -r 648fe09330f3 -r 3d8b37b1d798 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Aug 17 14:42:20 2022 +0200 @@ -157,7 +157,7 @@ def find_theory_node(theory: String): Option[Document.Node.Name] = { val thy_file = Path.basic(Long_Name.base_name(theory)).thy - val session = session_base.theory_qualifier(theory) + val session = sessions_structure.theory_qualifier(theory) val dirs = sessions_structure.get(session) match { case Some(info) => info.dirs @@ -182,7 +182,7 @@ } def import_name(name: Document.Node.Name, s: String): Document.Node.Name = - import_name(session_base.theory_qualifier(name), name.master_dir, s) + import_name(sessions_structure.theory_qualifier(name), name.master_dir, s) def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) @@ -198,7 +198,7 @@ } def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = { - val context_session = session_base.theory_qualifier(context_name) + val context_session = sessions_structure.theory_qualifier(context_name) val context_dir = try { Some(context_name.master_dir_path) } catch { case ERROR(_) => None } diff -r 648fe09330f3 -r 3d8b37b1d798 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Pure/Thy/presentation.scala Wed Aug 17 14:42:20 2022 +0200 @@ -17,19 +17,26 @@ /* HTML context */ - sealed case class HTML_Document(title: String, content: String) + def html_context( + sessions_structure: Sessions.Structure, + root_dir: Path = Path.current, + nodes: Nodes = Nodes.empty + ): HTML_Context = new HTML_Context(sessions_structure, root_dir, nodes) - abstract class HTML_Context { + class HTML_Context private[Presentation]( + sessions_structure: Sessions.Structure, + val root_dir: Path, + val nodes: Nodes + ) { /* directory structure and resources */ - def nodes: Nodes - def root_dir: Path - def theory_session(name: Document.Node.Name): Sessions.Info + def theory_session_info(name: Document.Node.Name): Sessions.Info = + sessions_structure(sessions_structure.theory_qualifier(name)) def session_dir(info: Sessions.Info): Path = root_dir + Path.explode(info.chapter_session) def theory_dir(name: Document.Node.Name): Path = - session_dir(theory_session(name)) + session_dir(theory_session_info(name)) def files_path(name: Document.Node.Name, path: Path): Path = theory_dir(name) + Path.explode("files") + path.squash.html @@ -63,6 +70,8 @@ } } + sealed case class HTML_Document(title: String, content: String) + /* presentation elements */ @@ -518,7 +527,7 @@ session0: String, node_name: Document.Node.Name ): Option[String] = { - val session1 = deps(session0).theory_qualifier(node_name) + val session1 = deps.sessions_structure.theory_qualifier(node_name) session_relative(deps, session0, session1) } @@ -619,7 +628,7 @@ make_html(entity_context(name), thy_elements, snapshot.xml_markup(elements = thy_elements.html))) - val thy_session = html_context.theory_session(name).name + val thy_session = html_context.theory_session_info(name).name val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name)) val files = for { (src_path, file_html) <- files_html } diff -r 648fe09330f3 -r 3d8b37b1d798 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Aug 17 14:42:20 2022 +0200 @@ -81,10 +81,6 @@ ", loaded_theories = " + loaded_theories.size + ", used_theories = " + used_theories.length + ")" - def theory_qualifier(name: String): String = - global_theories.getOrElse(name, Long_Name.qualifier(name)) - def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory) - def loaded_theory(name: String): Boolean = loaded_theories.defined(name) def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory) @@ -183,7 +179,8 @@ val overall_syntax = dependencies.overall_syntax val proper_session_theories = - dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name) + dependencies.theories.filter(name => + sessions_structure.theory_qualifier(name) == session_name) val theory_files = dependencies.theories.map(_.path) @@ -213,7 +210,7 @@ Graph_Display.Node("[" + name + "]", "session." + name) def node(name: Document.Node.Name): Graph_Display.Node = { - val qualifier = deps_base.theory_qualifier(name) + val qualifier = sessions_structure.theory_qualifier(name) if (qualifier == info.name) Graph_Display.Node(name.theory_base_name, "theory." + name.theory) else session_node(qualifier) @@ -221,7 +218,7 @@ val required_sessions = dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) - .map(theory => deps_base.theory_qualifier(theory)) + .map(theory => sessions_structure.theory_qualifier(theory)) .filter(name => name != info.name && sessions_structure.defined(name)) val required_subgraph = @@ -258,7 +255,7 @@ sessions_structure.imports_requirements(List(session_name)).toSet for { name <- dependencies.theories - qualifier = deps_base.theory_qualifier(name) + qualifier = sessions_structure.theory_qualifier(name) if !known_sessions(qualifier) } yield "Bad import of theory " + quote(name.toString) + ": need to include sessions " + quote(qualifier) + " in ROOT" @@ -280,7 +277,7 @@ known_theories.get(thy).map(_.name) match { case None => err("Unknown document theory") case Some(name) => - val qualifier = deps_base.theory_qualifier(name) + val qualifier = sessions_structure.theory_qualifier(name) if (proper_session_theories.contains(name)) { err("Redundant document theory from this session:") } @@ -413,7 +410,7 @@ val required_theories = for { thy <- base.loaded_theories.keys - if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session + if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session } yield thy @@ -764,6 +761,7 @@ def theory_qualifier(name: String): String = global_theories.getOrElse(name, Long_Name.qualifier(name)) + def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory) def check_sessions(names: List[String]): Unit = { val bad_sessions = SortedSet(names.filterNot(defined): _*).toList diff -r 648fe09330f3 -r 3d8b37b1d798 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Pure/Tools/build.scala Wed Aug 17 14:42:20 2022 +0200 @@ -504,12 +504,10 @@ progress.echo("Presenting " + session + " ...") val html_context = - new Presentation.HTML_Context { - override def nodes: Presentation.Nodes = presentation_nodes - override def root_dir: Path = presentation_dir - override def theory_session(name: Document.Node.Name): Sessions.Info = - deps.sessions_structure(deps(session).theory_qualifier(name)) - } + Presentation.html_context( + sessions_structure = deps.sessions_structure, + root_dir = presentation_dir, + nodes = presentation_nodes) using(database_context.open_session(deps.base_info(session))) { session_context => Presentation.session_html(session_context, deps, diff -r 648fe09330f3 -r 3d8b37b1d798 src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Tools/VSCode/src/preview_panel.scala Wed Aug 17 14:42:20 2022 +0200 @@ -28,13 +28,7 @@ val snapshot = model.snapshot() if (snapshot.is_outdated) m else { - val html_context = - new Presentation.HTML_Context { - override def nodes: Presentation.Nodes = Presentation.Nodes.empty - override def root_dir: Path = Path.current - override def theory_session(name: Document.Node.Name): Sessions.Info = - resources.sessions_structure(resources.session_base.theory_qualifier(name)) - } + val html_context = Presentation.html_context(resources.sessions_structure) val document = Presentation.html_document(snapshot, html_context, Presentation.elements2) channel.write(LSP.Preview_Response(file, column, document.title, document.content)) diff -r 648fe09330f3 -r 3d8b37b1d798 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 17 14:42:20 2022 +0200 @@ -313,14 +313,7 @@ } yield { val snapshot = model.await_stable_snapshot() - val html_context = - new Presentation.HTML_Context { - override def nodes: Presentation.Nodes = Presentation.Nodes.empty - override def root_dir: Path = Path.current - override def theory_session(name: Document.Node.Name): Sessions.Info = - PIDE.resources.sessions_structure( - PIDE.resources.session_base.theory_qualifier(name)) - } + val html_context = Presentation.html_context(PIDE.resources.sessions_structure) val document = Presentation.html_document( snapshot, html_context, Presentation.elements2, diff -r 648fe09330f3 -r 3d8b37b1d798 src/Tools/jEdit/src/isabelle_session.scala --- a/src/Tools/jEdit/src/isabelle_session.scala Wed Aug 17 11:57:13 2022 +0200 +++ b/src/Tools/jEdit/src/isabelle_session.scala Wed Aug 17 14:42:20 2022 +0200 @@ -84,10 +84,10 @@ PIDE.maybe_snapshot(view) match { case None => "" case Some(snapshot) => - val sessions = JEdit_Sessions.sessions_structure() - val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name) + val sessions_structure = JEdit_Sessions.sessions_structure() + val session = sessions_structure.theory_qualifier(snapshot.node_name) val chapter = - sessions.get(session) match { + sessions_structure.get(session) match { case Some(info) => info.chapter case None => Sessions.UNSORTED }