| 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 | 
 | 
| 75393 |     13 | object Flarum {
 | 
| 74945 |     14 |   // see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
 | 
| 74961 |     15 |   val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
 | 
| 74945 |     16 | 
 | 
|  |     17 |   def server(url: URL): Server = new Server(url)
 | 
|  |     18 | 
 | 
| 75393 |     19 |   class Server private[Flarum](url: URL) extends JSON_API.Service(url) {
 | 
| 74962 |     20 |     def get_api(route: String): JSON_API.Root =
 | 
|  |     21 |       get_root("api" + (if (route.isEmpty) "" else "/" + route))
 | 
| 74945 |     22 | 
 | 
| 74962 |     23 |     val root: JSON_API.Root = get_api("")
 | 
|  |     24 |     def users: JSON_API.Root = get_api("users")
 | 
|  |     25 |     def groups: JSON_API.Root = get_api("groups")
 | 
|  |     26 |     def discussions: JSON_API.Root = get_api("discussions")
 | 
| 74945 |     27 |   }
 | 
|  |     28 | }
 |