# HG changeset patch
# User wenzelm
# Date 1639606721 -3600
# Node ID 0dd14d8b16da51396b68ce0c7e8336c9f4bdddf7
# Parent  4dc90b43ba947ec5a0d880d36c5ada4812ae71bb
support for JSON:API;

diff -r 4dc90b43ba94 -r 0dd14d8b16da etc/build.props
--- a/etc/build.props	Wed Dec 15 19:41:30 2021 +0100
+++ b/etc/build.props	Wed Dec 15 23:18:41 2021 +0100
@@ -67,6 +67,7 @@
   src/Pure/General/graphics_file.scala \
   src/Pure/General/http.scala \
   src/Pure/General/json.scala \
+  src/Pure/General/json_api.scala \
   src/Pure/General/linear_set.scala \
   src/Pure/General/logger.scala \
   src/Pure/General/long_name.scala \
diff -r 4dc90b43ba94 -r 0dd14d8b16da src/Pure/General/json_api.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/json_api.scala	Wed Dec 15 23:18:41 2021 +0100
@@ -0,0 +1,76 @@
+/*  Title:      Pure/General/json_api.scala
+    Author:     Makarius
+
+Support for JSON:API: https://jsonapi.org/format
+*/
+
+package isabelle
+
+
+object JSON_API
+{
+  val mime_type = "application/vnd.api+json"
+
+  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  "))
+
+  sealed case class Root(json: JSON.T)
+  {
+    def get_links: Option[Links] = JSON.value(json, "links").map(Links)
+    def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
+    def get_data: Option[Data] = JSON.value(json, "data").map(Data(_, get_included))
+    def get_errors: Option[List[JSON.T]] = JSON.list(json, "errors", Some(_))
+
+    def ok: Boolean = get_errors.isEmpty
+    def check: Root =
+      get_errors match {
+        case None => this
+        case Some(List(err)) => api_error(JSON.Format(err))
+        case Some(errs) => api_errors(errs.map(JSON.Format.apply))
+      }
+    def check_data: Data = check.get_data getOrElse api_error("missing data")
+
+    override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
+  }
+
+  sealed case class Links(json: JSON.T)
+  {
+    def get_next: Option[Root] =
+      for (next <- JSON.value(json, "next") if next != null) yield Root(next)
+
+    override def toString: String =
+      if (get_next.isEmpty) "Links()" else "Links(next)"
+  }
+
+  sealed case class Data(data: JSON.T, included: List[Resource])
+  {
+    def is_multi: Boolean = JSON.Value.List.unapply(data, Some(_)).nonEmpty
+
+    def resource: Resource =
+      if (is_multi) api_error("singleton resource expected")
+      else Resource.some(data).get
+
+    def resources: List[Resource] =
+      JSON.Value.List.unapply(data, Resource.some)
+        .getOrElse(api_error("multiple resources expected"))
+
+    override def toString: String =
+      if (is_multi) "Data(resources)" else "Data(resource)"
+  }
+
+  object Resource
+  {
+    def some(json: JSON.T): Some[Resource] = Some(Resource(json))
+  }
+
+  sealed case class Resource(json: JSON.T)
+  {
+    val id: JSON.T = JSON.value(json, "id") getOrElse api_error("missing id")
+    val type_ : JSON.T = JSON.value(json, "type") getOrElse api_error("missing type")
+    val fields: JSON.Object.T =
+      JSON.value(json, "attributes", JSON.Object.unapply).getOrElse(JSON.Object.empty) ++
+      JSON.value(json, "relationships", JSON.Object.unapply).getOrElse(JSON.Object.empty)
+
+    override def toString: String = JSON.Format(json)
+  }
+}
diff -r 4dc90b43ba94 -r 0dd14d8b16da src/Pure/Tools/flarum.scala
--- a/src/Pure/Tools/flarum.scala	Wed Dec 15 19:41:30 2021 +0100
+++ b/src/Pure/Tools/flarum.scala	Wed Dec 15 23:18:41 2021 +0100
@@ -22,8 +22,11 @@
     override def toString: String = url.toString
 
     def get(route: String): HTTP.Content =
-      HTTP.Client.get(new URL(url, route))
+      HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
 
-    val api: JSON.T = get("api").json
+    def get_api(route: String = ""): JSON_API.Root =
+      JSON_API.Root(get("api" + (if (route.isEmpty) "" else "/" + route)).json)
+
+    val api: JSON_API.Root = get_api()
   }
 }