--- a/src/Pure/General/json_api.scala Sun Jan 21 13:18:05 2024 +0100
+++ b/src/Pure/General/json_api.scala Sun Jan 21 14:05:14 2024 +0100
@@ -6,8 +6,6 @@
package isabelle
-import java.net.URL
-
object JSON_API {
val mime_type = "application/vnd.api+json"
@@ -15,11 +13,11 @@
def api_error(msg: String): Nothing = error("JSON API error: " + msg)
def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n "))
- class Service(val url: URL) {
+ class Service(val url: Url) {
override def toString: String = url.toString
def get(route: String): HTTP.Content =
- HTTP.Client.get(Url.resolve(url, route))
+ HTTP.Client.get(url.resolve(route))
def get_root(route: String = ""): Root =
Root(get(if_proper(route, "/" + route)).json)