# HG changeset patch
# User wenzelm
# Date 1645796296 -3600
# Node ID e721880779bed268db28130114b911c83c6fbd9d
# Parent  883d610a1a91518c339d32b10edbce7bd8870883
clarified signature;

diff -r 883d610a1a91 -r e721880779be src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Fri Feb 25 14:02:59 2022 +0100
+++ b/src/Pure/General/http.scala	Fri Feb 25 14:38:16 2022 +0100
@@ -302,11 +302,13 @@
   /** Isabelle services **/
 
   def isabelle_services: List[Service] =
-    List(new Welcome(), new Fonts(), new PDFjs(), new Docs())
+    List(Welcome_Service, Fonts_Service, PDFjs_Service, Docs_Service)
 
 
   /* welcome */
 
+  object Welcome_Service extends Welcome()
+
   class Welcome(name: String = "") extends Service(name)
   {
     def apply(request: Request): Option[Response] =
@@ -319,6 +321,8 @@
 
   /* fonts */
 
+  object Fonts_Service extends Fonts()
+
   class Fonts(name: String = "fonts") extends Service(name)
   {
     private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
@@ -339,6 +343,8 @@
 
   /* pdfjs */
 
+  object PDFjs_Service extends PDFjs()
+
   class PDFjs(name: String = "pdfjs") extends Service(name)
   {
     def apply(request: Request): Option[Response] =
@@ -352,6 +358,8 @@
 
   /* docs */
 
+  object Docs_Service extends Docs()
+
   class Docs(name: String = "docs") extends PDFjs(name)
   {
     private val doc_contents = isabelle.Doc.main_contents()
diff -r 883d610a1a91 -r e721880779be src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Feb 25 14:02:59 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Feb 25 14:38:16 2022 +0100
@@ -303,14 +303,14 @@
       case Some(model) =>
         val name = model.node_name
         val url =
-          PIDE.plugin.http_server.url + "/" + Preview.service + "?" +
+          PIDE.plugin.http_server.url + "/" + Preview_Service.service + "?" +
               (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
   }
 
-  object Preview extends HTTP.Service("preview")
+  object Preview_Service extends HTTP.Service("preview")
   {
     def apply(request: HTTP.Request): Option[HTTP.Response] =
       for {
diff -r 883d610a1a91 -r e721880779be src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Fri Feb 25 14:02:59 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Fri Feb 25 14:38:16 2022 +0100
@@ -430,7 +430,7 @@
   val http_root: String = "/" + UUID.random().toString
 
   val http_server: HTTP.Server =
-    HTTP.server(services = Document_Model.Preview :: HTTP.isabelle_services)
+    HTTP.server(services = Document_Model.Preview_Service :: HTTP.isabelle_services)
 
 
   /* start and stop */