--- a/src/Pure/General/http.scala Fri Feb 25 14:38:16 2022 +0100
+++ b/src/Pure/General/http.scala Fri Feb 25 14:42:38 2022 +0100
@@ -174,12 +174,12 @@
names.iterator.flatMap(a => if (a.isEmpty) None else Some("/" + a)).mkString
class Request private[HTTP](
- val server: String,
- val service: String,
+ val server_name: String,
+ val service_name: String,
val uri: URI,
val input: Bytes)
{
- def home: String = url_path(server, service)
+ def home: String = url_path(server_name, service_name)
def root: String = home + "/"
def query: String = home + "?"
@@ -239,19 +239,20 @@
/* service */
- abstract class Service(val service: String, method: String = "GET")
+ abstract class Service(val name: String, method: String = "GET")
{
- override def toString: String = service
+ override def toString: String = name
def apply(request: Request): Option[Response]
- def context(server: String): String = proper_string(url_path(server, service)).getOrElse("/")
+ def context(server_name: String): String =
+ proper_string(url_path(server_name, name)).getOrElse("/")
- def handler(server: String): HttpHandler = (http: HttpExchange) => {
+ def handler(server_name: String): HttpHandler = (http: HttpExchange) => {
val uri = http.getRequestURI
val input = using(http.getRequestBody)(Bytes.read_stream(_))
if (http.getRequestMethod == method) {
- val request = new Request(server, service, uri, input)
+ val request = new Request(server_name, name, uri, input)
Exn.capture(apply(request)) match {
case Exn.Res(Some(response)) =>
response.write(http, 200)
--- a/src/Tools/jEdit/src/document_model.scala Fri Feb 25 14:38:16 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Feb 25 14:42:38 2022 +0100
@@ -303,7 +303,7 @@
case Some(model) =>
val name = model.node_name
val url =
- PIDE.plugin.http_server.url + "/" + Preview_Service.service + "?" +
+ PIDE.plugin.http_server.url + "/" + Preview_Service.name + "?" +
(if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
@@ -332,7 +332,7 @@
Presentation.html_document(
snapshot, html_context, Presentation.elements2,
plain_text = query.startsWith(plain_text_prefix),
- fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server)))
+ fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
HTTP.Response.html(document.content)
}
}