--- a/src/Pure/PIDE/document_status.scala Thu Nov 11 21:54:28 2021 +0100
+++ b/src/Pure/PIDE/document_status.scala Thu Nov 11 22:06:18 2021 +0100
@@ -268,7 +268,7 @@
val update_iterator =
for {
name <- domain.getOrElse(nodes1.domain).iterator
- if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
+ if !Resources.hidden_node(name) && !resources.session_base.loaded_theory(name)
st = Document_Status.Node_Status.make(state, version, name)
if !rep.isDefinedAt(name) || rep(name) != st
} yield (name -> st)
--- a/src/Pure/PIDE/resources.scala Thu Nov 11 21:54:28 2021 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Nov 11 22:06:18 2021 +0100
@@ -19,6 +19,12 @@
def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
empty.file_node(file, dir = dir, theory = theory)
+
+ def hidden_node(name: Document.Node.Name): Boolean =
+ !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
+
+ def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
+ File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
}
class Resources(
@@ -63,12 +69,6 @@
def make_theory_content(thy_name: Document.Node.Name): Option[String] =
File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
- def is_hidden(name: Document.Node.Name): Boolean =
- !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
-
- def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
- File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
-
/* file-system operations */
--- a/src/Pure/Thy/presentation.scala Thu Nov 11 21:54:28 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Thu Nov 11 22:06:18 2021 +0100
@@ -269,7 +269,6 @@
/* PIDE HTML document */
def html_document(
- resources: Resources,
snapshot: Document.Snapshot,
html_context: HTML_Context,
elements: Elements,
@@ -285,7 +284,7 @@
html_context.html_document(title, body, fonts_css)
}
else {
- resources.html_document(snapshot) getOrElse {
+ Resources.html_document(snapshot) getOrElse {
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
--- a/src/Tools/VSCode/src/preview_panel.scala Thu Nov 11 21:54:28 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Thu Nov 11 22:06:18 2021 +0100
@@ -33,8 +33,7 @@
else {
val html_context = Presentation.html_context()
val document =
- Presentation.html_document(
- resources, snapshot, html_context, Presentation.elements2)
+ Presentation.html_document(snapshot, html_context, Presentation.elements2)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
--- a/src/Tools/jEdit/src/document_model.scala Thu Nov 11 21:54:28 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Nov 11 22:06:18 2021 +0100
@@ -327,7 +327,7 @@
val html_context = Presentation.html_context()
val document =
Presentation.html_document(
- PIDE.resources, snapshot, html_context, Presentation.elements2,
+ snapshot, html_context, Presentation.elements2,
plain_text = query.startsWith(plain_text_prefix),
fonts_css = HTML.fonts_css_dir(http_root))
HTTP.Response.html(document.content)