74945
|
1 |
/* Title: Pure/General/flarum.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for Flarum forum server: https://flarum.org
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
import java.net.URL
|
|
11 |
|
|
12 |
|
|
13 |
object Flarum
|
|
14 |
{
|
|
15 |
// see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
|
|
16 |
val Date_Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
|
|
17 |
|
|
18 |
def server(url: URL): Server = new Server(url)
|
|
19 |
|
|
20 |
class Server private[Flarum](url: URL)
|
|
21 |
{
|
|
22 |
override def toString: String = url.toString
|
|
23 |
|
|
24 |
def get(route: String): HTTP.Content =
|
74946
|
25 |
HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
|
74945
|
26 |
|
74946
|
27 |
def get_api(route: String = ""): JSON_API.Root =
|
|
28 |
JSON_API.Root(get("api" + (if (route.isEmpty) "" else "/" + route)).json)
|
|
29 |
|
|
30 |
val api: JSON_API.Root = get_api()
|
74945
|
31 |
}
|
|
32 |
}
|