clarified signature: prefer static operations;
authorwenzelm
Thu, 11 Nov 2021 22:06:18 +0100
changeset 74756 a6c7a257b713
parent 74755 510296c0d8d1
child 74757 2e3b649111f1
clarified signature: prefer static operations;
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/presentation.scala
src/Tools/VSCode/src/preview_panel.scala
src/Tools/jEdit/src/document_model.scala
--- 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)