--- a/src/Pure/General/http.scala Mon Feb 21 13:30:51 2022 +0100
+++ b/src/Pure/General/http.scala Mon Feb 21 14:33:41 2022 +0100
@@ -239,41 +239,31 @@
/* service */
- type Exchange = Request => Option[Response]
-
- object Service
+ abstract class Service(val service: String, method: String = "GET")
{
- def apply(method: String, name: String, body: Exchange): Service =
- new Service(name: String) {
- def handler(server: 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, name, uri, input)
- Exn.capture(body(request)) match {
- case Exn.Res(Some(response)) =>
- response.write(http, 200)
- case Exn.Res(None) =>
- Response.empty.write(http, 404)
- case Exn.Exn(ERROR(msg)) =>
- Response.text(Output.error_message_text(msg)).write(http, 500)
- case Exn.Exn(exn) => throw exn
- }
- }
- else Response.empty.write(http, 400)
+ override def toString: String = service
+
+ def apply(request: Request): Option[Response]
+
+ def context(server: String): String = proper_string(url_path(server, service)).getOrElse("/")
+
+ def handler(server: 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)
+ Exn.capture(apply(request)) match {
+ case Exn.Res(Some(response)) =>
+ response.write(http, 200)
+ case Exn.Res(None) =>
+ Response.empty.write(http, 404)
+ case Exn.Exn(ERROR(msg)) =>
+ Response.text(Output.error_message_text(msg)).write(http, 500)
+ case Exn.Exn(exn) => throw exn
}
+ }
+ else Response.empty.write(http, 400)
}
-
- def get(name: String, body: Exchange): Service = apply("GET", name, body)
- def post(name: String, body: Exchange): Service = apply("POST", name, body)
- }
-
- abstract class Service private[HTTP](val name: String)
- {
- override def toString: String = name
- def context(server: String): String = proper_string(url_path(server, name)).getOrElse("/")
- def handler(server: String): HttpHandler
}
@@ -311,48 +301,51 @@
/** Isabelle services **/
- def isabelle_services: List[Service] = List(welcome(), fonts(), pdfjs())
+ def isabelle_services: List[Service] =
+ List(new Welcome(), new Fonts(), new PDFjs())
/* welcome */
- def welcome(name: String = ""): Service =
- Service.get(name, request =>
- {
- if (request.toplevel) {
- Some(Response.text("Welcome to " + Isabelle_System.identification()))
- }
- else None
- })
+ class Welcome(name: String = "") extends Service(name)
+ {
+ def apply(request: Request): Option[Response] =
+ if (request.toplevel) {
+ Some(Response.text("Welcome to " + Isabelle_System.identification()))
+ }
+ else None
+ }
/* fonts */
- private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
- Isabelle_Fonts.fonts(hidden = true)
+ class Fonts(name: String = "fonts") extends Service(name)
+ {
+ private lazy val html_fonts: List[Isabelle_Fonts.Entry] =
+ Isabelle_Fonts.fonts(hidden = true)
- def fonts(name: String = "fonts"): Service =
- Service.get(name, request =>
- {
- if (request.toplevel) {
- Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
- }
- else {
- request.uri_path.flatMap(path =>
- html_fonts.collectFirst(
- { case entry if path == entry.path.base => Response(entry.bytes) }
- ))
- }
- })
+ def apply(request: Request): Option[Response] =
+ if (request.toplevel) {
+ Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.file_name))))
+ }
+ else {
+ request.uri_path.flatMap(path =>
+ html_fonts.collectFirst(
+ { case entry if path == entry.path.base => Response(entry.bytes) }
+ ))
+ }
+ }
/* pdfjs */
- def pdfjs(name: String = "pdfjs"): Service =
- Service.get(name, request =>
+ class PDFjs(name: String = "pdfjs") extends Service(name)
+ {
+ def apply(request: Request): Option[Response] =
for {
p <- request.uri_path
path = Path.explode("$ISABELLE_PDFJS_HOME") + p
if path.is_file
- } yield Response.read(path))
+ } yield Response.read(path)
+ }
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/document_model.scala Mon Feb 21 13:30:51 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Feb 21 14:33:41 2022 +0100
@@ -303,15 +303,16 @@
case Some(model) =>
val name = model.node_name
val url =
- PIDE.plugin.http_server.url + "/preview?" +
- (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
+ PIDE.plugin.http_server.url + "/" + Preview.service + "?" +
+ (if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
}
}
- def preview_service: HTTP.Service =
- HTTP.Service.get("preview", request =>
+ object Preview extends HTTP.Service("preview")
+ {
+ def apply(request: HTTP.Request): Option[HTTP.Response] =
for {
query <- request.decode_query
name = Library.perhaps_unprefix(plain_text_prefix, query)
@@ -322,6 +323,7 @@
val html_context =
new Presentation.HTML_Context {
override def root_dir: Path = Path.current
+
override def theory_session(name: Document.Node.Name): Sessions.Info =
PIDE.resources.sessions_structure(
PIDE.resources.session_base.theory_qualifier(name))
@@ -332,7 +334,8 @@
plain_text = query.startsWith(plain_text_prefix),
fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server)))
HTTP.Response.html(document.content)
- })
+ }
+ }
}
sealed abstract class Document_Model extends Document.Model
--- a/src/Tools/jEdit/src/main_plugin.scala Mon Feb 21 13:30:51 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala Mon Feb 21 14:33:41 2022 +0100
@@ -430,7 +430,7 @@
val http_root: String = "/" + UUID.random().toString
val http_server: HTTP.Server =
- HTTP.server(services = Document_Model.preview_service :: HTTP.isabelle_services)
+ HTTP.server(services = Document_Model.Preview :: HTTP.isabelle_services)
/* start and stop */