src/Pure/PIDE/resources.scala
changeset 75941 4bbbbaa656f1
parent 75922 b327e5d5d6b4
child 76046 507c65cc4332
--- a/src/Pure/PIDE/resources.scala	Sun Aug 21 11:52:51 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Sun Aug 21 11:59:25 2022 +0200
@@ -19,7 +19,7 @@
   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] =
+  def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] =
     File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
 }