# HG changeset patch
# User wenzelm
# Date 1736687670 -3600
# Node ID 10669f47f6fd5b9bcda8b80408bd162317a053a9
# Parent  e06819faea88048f85ef826f1492dfc988e891e6
clarified signature and modules;

diff -r e06819faea88 -r 10669f47f6fd src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sun Jan 12 14:08:02 2025 +0100
+++ b/src/Pure/General/http.scala	Sun Jan 12 14:14:30 2025 +0100
@@ -1,5 +1,6 @@
 /*  Title:      Pure/General/http.scala
     Author:     Makarius
+    Author:     Fabian Huch, TU München
 
 HTTP client and server support.
 */
@@ -264,6 +265,42 @@
   }
 
 
+  /* REST service (via JSON) */
+
+  abstract class REST_Service(
+    name: String,
+    progress: Progress = new Progress,
+    method: String = "POST"
+  ) extends Service(name, method = method) {
+    def handle(body: JSON.T): Option[JSON.T]
+
+    def apply(request: Request): Option[Response] =
+      try {
+        for {
+          json <-
+            Exn.capture(JSON.parse(request.input.text)) match {
+              case Exn.Res(json) => Some(json)
+              case _ =>
+                progress.echo("Could not parse: " + quote(request.input.text), verbose = true)
+                None
+            }
+          res <-
+            handle(json) match {
+              case Some(res) => Some(res)
+              case None =>
+                progress.echo("Invalid request: " + JSON.Format(json), verbose = true)
+                None
+            }
+        } yield Response(Bytes(JSON.Format(res)), content_type = "application/json")
+      }
+      catch { case exn: Throwable =>
+        val uuid = UUID.random()
+        progress.echo_error_message("Server error <" + uuid + ">: " + exn)
+        Some(Response.text("internal server error: " + uuid))
+      }
+  }
+
+
   /* server */
 
   class Server private[HTTP](val name: String, val http_server: HttpServer) {
diff -r e06819faea88 -r 10669f47f6fd src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 14:08:02 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 14:14:30 2025 +0100
@@ -814,36 +814,6 @@
 
   /* find facts */
 
-  abstract class REST_Service(path: Path, progress: Progress, method: String = "POST")
-    extends HTTP.Service(path.implode, method = method) {
-    def handle(body: JSON.T): Option[JSON.T]
-
-    def apply(request: HTTP.Request): Option[HTTP.Response] =
-      try {
-        for {
-          json <-
-            Exn.capture(JSON.parse(request.input.text)) match {
-              case Exn.Res(json) => Some(json)
-              case _ =>
-                progress.echo("Could not parse: " + quote(request.input.text), verbose = true)
-                None
-            }
-          res <-
-            handle(json) match {
-              case Some(res) => Some(res)
-              case None =>
-                progress.echo("Invalid request: " + JSON.Format(json), verbose = true)
-                None
-            }
-        } yield HTTP.Response(Bytes(JSON.Format(res)), content_type = "application/json")
-      }
-      catch { case exn: Throwable =>
-        val uuid = UUID.random()
-        progress.echo_error_message("Server error <" + uuid + ">: " + exn)
-        Some(HTTP.Response.text("internal server error: " + uuid))
-      }
-  }
-
   def find_facts(
     options: Options,
     port: Int,
@@ -884,19 +854,19 @@
             def apply(request: HTTP.Request): Option[HTTP.Response] =
               Some(HTTP.Response.html(if (devel) project.build_html(progress) else frontend))
           },
-          new REST_Service(Path.explode("api/block"), progress) {
+          new HTTP.REST_Service("api/block", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =
               for {
                 request <- Parse.query_block(body)
                 block <- query_block(db, request)
               } yield encode.block(block)
           },
-          new REST_Service(Path.explode("api/blocks"), progress) {
+          new HTTP.REST_Service("api/blocks", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =
               for (request <- Parse.query_blocks(body))
               yield encode.blocks(query_blocks(db, request.query, Some(request.cursor)))
           },
-          new REST_Service(Path.explode("api/query"), progress) {
+          new HTTP.REST_Service("api/query", progress = progress) {
             def handle(body: JSON.T): Option[JSON.T] =
               for (query <- Parse.query(body)) yield {
                 val facet = query_facet(db, query)