# HG changeset patch
# User wenzelm
# Date 1645446651 -3600
# Node ID 899e70a9af83494654da8a051ae6860d58597073
# Parent  ecaac5050ec2f307a2f211bb5201a24cc8993b63
tuned signature;

diff -r ecaac5050ec2 -r 899e70a9af83 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Feb 21 13:19:30 2022 +0100
+++ b/src/Pure/General/http.scala	Mon Feb 21 13:30:51 2022 +0100
@@ -194,6 +194,9 @@
         p = Path.explode(s) if p.all_basic
       } yield p
 
+    def decode_query: Option[String] =
+      Library.try_unprefix(query, uri_name).map(Url.decode)
+
     def decode_properties: Properties.T =
       space_explode('&', input.text).map(
         {
diff -r ecaac5050ec2 -r 899e70a9af83 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Feb 21 13:19:30 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Feb 21 13:30:51 2022 +0100
@@ -313,7 +313,7 @@
   def preview_service: HTTP.Service =
     HTTP.Service.get("preview", request =>
       for {
-        query <- Library.try_unprefix(request.query, request.uri_name).map(Url.decode)
+        query <- request.decode_query
         name = Library.perhaps_unprefix(plain_text_prefix, query)
         model <- get(PIDE.resources.node_name(name))
       }