--- 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()
--- 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 {
--- 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 */