# HG changeset patch
# User wenzelm
# Date 1661078145 -7200
# Node ID abc3e052ba5d68e815faef711cecbc4c7b56f4c6
# Parent  367194f280b7ebebea9408a896ded8e37d0e5d00
clarified signature;

diff -r 367194f280b7 -r abc3e052ba5d src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:23:17 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 21 12:35:45 2022 +0200
@@ -98,6 +98,9 @@
       else List(HTML.div(css_class, List(HTML.section(heading), HTML.itemize(items))))
     }
 
+
+    /* preview PIDE document */
+
     val isabelle_css: String = File.read(HTML.isabelle_css)
 
     def html_document(title: String, body: XML.Body, fonts_css: String): HTML_Document = {
@@ -109,6 +112,31 @@
           List(HTML.source(body)), css = "", structural = false)
       HTML_Document(title, content)
     }
+
+    def preview_document(
+      snapshot: Document.Snapshot,
+      plain_text: Boolean = false,
+      fonts_css: String = HTML.fonts_css()
+    ): HTML_Document = {
+      require(!snapshot.is_outdated, "document snapshot outdated")
+
+      val name = snapshot.node_name
+      if (plain_text) {
+        val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
+        val body = HTML.text(snapshot.node.source)
+        html_document(title, body, fonts_css)
+      }
+      else {
+        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)
+          val xml = snapshot.xml_markup(elements = elements.html)
+          val body = Node_Context.empty.make_html(elements, xml)
+          html_document(title, body, fonts_css)
+        }
+      }
+    }
   }
 
   sealed case class HTML_Document(title: String, content: String)
@@ -307,35 +335,6 @@
   }
 
 
-  /* PIDE HTML document */
-
-  def html_document(
-    snapshot: Document.Snapshot,
-    context: Context,
-    plain_text: Boolean = false,
-    fonts_css: String = HTML.fonts_css()
-  ): HTML_Document = {
-    require(!snapshot.is_outdated, "document snapshot outdated")
-
-    val name = snapshot.node_name
-    if (plain_text) {
-      val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
-      val body = HTML.text(snapshot.node.source)
-      context.html_document(title, body, fonts_css)
-    }
-    else {
-      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)
-        val xml = snapshot.xml_markup(elements = context.elements.html)
-        val body = Node_Context.empty.make_html(context.elements, xml)
-        context.html_document(title, body, fonts_css)
-      }
-    }
-  }
-
-
 
   /** HTML presentation **/
 
diff -r 367194f280b7 -r abc3e052ba5d src/Tools/VSCode/src/preview_panel.scala
--- a/src/Tools/VSCode/src/preview_panel.scala	Sun Aug 21 12:23:17 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala	Sun Aug 21 12:35:45 2022 +0200
@@ -28,9 +28,9 @@
                 val snapshot = model.snapshot()
                 if (snapshot.is_outdated) m
                 else {
-                  val context =
-                    Browser_Info.context(resources.sessions_structure, Browser_Info.elements2)
-                  val document = Browser_Info.html_document(snapshot, context)
+                  val document =
+                    Browser_Info.context(resources.sessions_structure, Browser_Info.elements2).
+                      preview_document(snapshot)
                   channel.write(LSP.Preview_Response(file, column, document.title, document.content))
                   m - file
                 }
diff -r 367194f280b7 -r abc3e052ba5d src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 12:23:17 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 12:35:45 2022 +0200
@@ -313,10 +313,9 @@
       }
       yield {
         val snapshot = model.await_stable_snapshot()
-        val context =
-          Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2)
         val document =
-          Browser_Info.html_document(snapshot, context,
+          Browser_Info.context(PIDE.resources.sessions_structure, Browser_Info.elements2).
+            preview_document(snapshot,
             plain_text = query.startsWith(plain_text_prefix),
             fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
         HTTP.Response.html(document.content)