# HG changeset patch
# User wenzelm
# Date 1645799586 -3600
# Node ID 90678a1929a31a28f871283d8478798b7a9033d2
# Parent  f9d2a9e94138b073aea603e1225977b7ec86d92e
clarified signature;

diff -r f9d2a9e94138 -r 90678a1929a3 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Feb 25 15:01:47 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Feb 25 15:33:06 2022 +0100
@@ -295,16 +295,11 @@
 
   /* HTTP preview */
 
-  private val plain_text_prefix = "plain_text="
-
   def open_preview(view: View, plain_text: Boolean): Unit =
   {
     Document_Model.get(view.getBuffer) match {
       case Some(model) =>
-        val name = model.node_name
-        val url =
-          PIDE.plugin.http_server.url + "/" + Preview_Service.name + "?" +
-              (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
+        val url = Preview_Service.server_url(plain_text, model.node_name)
         PIDE.editor.hyperlink_url(url).follow(view)
       case _ =>
     }
@@ -312,6 +307,14 @@
 
   object Preview_Service extends HTTP.Service("preview")
   {
+    service =>
+
+    private val plain_text_prefix = "plain_text="
+
+    def server_url(plain_text: Boolean, node_name: Document.Node.Name): String =
+      PIDE.plugin.http_server.url + "/" + service.name + "?" +
+        (if (plain_text) plain_text_prefix else "") + Url.encode(node_name.node)
+
     def apply(request: HTTP.Request): Option[HTTP.Response] =
       for {
         query <- request.decode_query