# HG changeset patch
# User wenzelm
# Date 1608375917 -3600
# Node ID c007d0fa0938a8975dc7e6c30997edc374ba12ce
# Parent  942bf91545fa949807ea22747dab0e57dd999540
tuned signature;

diff -r 942bf91545fa -r c007d0fa0938 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Dec 19 11:43:24 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 19 12:05:17 2020 +0100
@@ -54,12 +54,12 @@
   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 make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
-    File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
-
   def is_hidden(name: Document.Node.Name): Boolean =
     !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
 
+  def file_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
+    File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
+
 
   /* file-system operations */
 
diff -r 942bf91545fa -r c007d0fa0938 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Dec 19 11:43:24 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Dec 19 12:05:17 2020 +0100
@@ -376,7 +376,7 @@
       Preview(title, content)
     }
     else {
-      resources.make_preview(snapshot) match {
+      resources.file_preview(snapshot) match {
         case Some(preview) => preview
         case None =>
           val title =