| author | wenzelm |
| Tue, 22 Oct 2024 12:45:38 +0200 | |
| changeset 81229 | e18600daa904 |
| parent 79510 | d8330439823a |
| permissions | -rw-r--r-- |
| 77570 | 1 |
/* Title: Pure/Tools/flarum.scala |
| 74945 | 2 |
Author: Makarius |
3 |
||
4 |
Support for Flarum forum server: https://flarum.org |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
| 75393 | 10 |
object Flarum {
|
| 74945 | 11 |
// see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php |
| 74961 | 12 |
val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
|
| 74945 | 13 |
|
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
77570
diff
changeset
|
14 |
def server(url: Url): Server = new Server(url) |
| 74945 | 15 |
|
|
79510
d8330439823a
clarified signature: explicit type isabelle.Url to avoid oddities of java.net.URL (e.g. its "equals" method);
wenzelm
parents:
77570
diff
changeset
|
16 |
class Server private[Flarum](url: Url) extends JSON_API.Service(url) {
|
| 76618 | 17 |
def get_api(route: String): JSON_API.Root = get_root(Url.append_path("api", route))
|
| 74962 | 18 |
val root: JSON_API.Root = get_api("")
|
19 |
def users: JSON_API.Root = get_api("users")
|
|
20 |
def groups: JSON_API.Root = get_api("groups")
|
|
21 |
def discussions: JSON_API.Root = get_api("discussions")
|
|
| 74945 | 22 |
} |
23 |
} |