74946
|
1 |
/* Title: Pure/General/json_api.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for JSON:API: https://jsonapi.org/format
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
74962
|
9 |
import java.net.URL
|
|
10 |
|
74946
|
11 |
|
75393
|
12 |
object JSON_API {
|
74946
|
13 |
val mime_type = "application/vnd.api+json"
|
|
14 |
|
|
15 |
def api_error(msg: String): Nothing = error("JSON API error: " + msg)
|
|
16 |
def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n "))
|
|
17 |
|
75393
|
18 |
class Service(val url: URL) {
|
74962
|
19 |
override def toString: String = url.toString
|
|
20 |
|
|
21 |
def get(route: String): HTTP.Content =
|
|
22 |
HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
|
|
23 |
|
|
24 |
def get_root(route: String = ""): Root =
|
77368
|
25 |
Root(get(if_proper(route, "/" + route)).json)
|
74962
|
26 |
}
|
|
27 |
|
75393
|
28 |
sealed case class Root(json: JSON.T) {
|
75403
|
29 |
def get_links: Option[Links] = JSON.value(json, "links").map(Links.apply)
|
74962
|
30 |
def get_next: Option[Service] = get_links.flatMap(_.get_next)
|
|
31 |
|
74946
|
32 |
def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
|
|
33 |
def get_data: Option[Data] = JSON.value(json, "data").map(Data(_, get_included))
|
74962
|
34 |
|
74946
|
35 |
def get_errors: Option[List[JSON.T]] = JSON.list(json, "errors", Some(_))
|
|
36 |
|
|
37 |
def ok: Boolean = get_errors.isEmpty
|
|
38 |
def check: Root =
|
|
39 |
get_errors match {
|
|
40 |
case None => this
|
|
41 |
case Some(List(err)) => api_error(JSON.Format(err))
|
|
42 |
case Some(errs) => api_errors(errs.map(JSON.Format.apply))
|
|
43 |
}
|
|
44 |
def check_data: Data = check.get_data getOrElse api_error("missing data")
|
74962
|
45 |
def check_resource: Resource = check_data.resource
|
|
46 |
def check_resources: List[Resource] = check_data.resources
|
74946
|
47 |
|
75393
|
48 |
def iterator: Iterator[Root] = {
|
74963
|
49 |
val init = Some(this)
|
|
50 |
new Iterator[Root] {
|
|
51 |
private var state: Option[Root] = init
|
|
52 |
def hasNext: Boolean = state.nonEmpty
|
|
53 |
def next(): Root =
|
|
54 |
state match {
|
|
55 |
case None => Iterator.empty.next()
|
|
56 |
case Some(res) =>
|
|
57 |
state = res.get_next.map(_.get_root())
|
|
58 |
res
|
|
59 |
}
|
|
60 |
}
|
|
61 |
}
|
|
62 |
def iterator_data: Iterator[Data] = iterator.map(_.check_data)
|
|
63 |
def iterator_resource: Iterator[Resource] = iterator.map(_.check_resource)
|
|
64 |
def iterator_resources: Iterator[Resource] = iterator.flatMap(_.check_resources)
|
|
65 |
|
74946
|
66 |
override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
|
|
67 |
}
|
|
68 |
|
75393
|
69 |
sealed case class Links(json: JSON.T) {
|
74962
|
70 |
def get_next: Option[Service] =
|
|
71 |
for {
|
|
72 |
JSON.Value.String(next) <- JSON.value(json, "next")
|
|
73 |
if Url.is_wellformed(next)
|
|
74 |
} yield new Service(Url(next))
|
74946
|
75 |
|
|
76 |
override def toString: String =
|
|
77 |
if (get_next.isEmpty) "Links()" else "Links(next)"
|
|
78 |
}
|
|
79 |
|
75393
|
80 |
sealed case class Data(data: JSON.T, included: List[Resource]) {
|
74946
|
81 |
def is_multi: Boolean = JSON.Value.List.unapply(data, Some(_)).nonEmpty
|
|
82 |
|
|
83 |
def resource: Resource =
|
|
84 |
if (is_multi) api_error("singleton resource expected")
|
|
85 |
else Resource.some(data).get
|
|
86 |
|
|
87 |
def resources: List[Resource] =
|
|
88 |
JSON.Value.List.unapply(data, Resource.some)
|
|
89 |
.getOrElse(api_error("multiple resources expected"))
|
|
90 |
|
|
91 |
override def toString: String =
|
|
92 |
if (is_multi) "Data(resources)" else "Data(resource)"
|
|
93 |
}
|
|
94 |
|
75393
|
95 |
object Resource {
|
74946
|
96 |
def some(json: JSON.T): Some[Resource] = Some(Resource(json))
|
|
97 |
}
|
|
98 |
|
75393
|
99 |
sealed case class Resource(json: JSON.T) {
|
74946
|
100 |
val id: JSON.T = JSON.value(json, "id") getOrElse api_error("missing id")
|
|
101 |
val type_ : JSON.T = JSON.value(json, "type") getOrElse api_error("missing type")
|
|
102 |
val fields: JSON.Object.T =
|
|
103 |
JSON.value(json, "attributes", JSON.Object.unapply).getOrElse(JSON.Object.empty) ++
|
|
104 |
JSON.value(json, "relationships", JSON.Object.unapply).getOrElse(JSON.Object.empty)
|
|
105 |
|
|
106 |
override def toString: String = JSON.Format(json)
|
|
107 |
}
|
|
108 |
}
|