src/Pure/General/json_api.scala
changeset 79510 d8330439823a
parent 79044 8cc1ae43e12e
--- 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)