--- 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(
{
--- 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))
}