src/Pure/Tools/flarum.scala
author wenzelm
Tue, 07 Mar 2023 23:24:40 +0100
changeset 77570 98b4a9902582
parent 76618 aeded421d374
child 79510 d8330439823a
permissions -rw-r--r--
tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77570
98b4a9902582 tuned headers;
wenzelm
parents: 76618
diff changeset
     1
/*  Title:      Pure/Tools/flarum.scala
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     3
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     4
Support for Flarum forum server: https://flarum.org
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     5
*/
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     6
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     7
package isabelle
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     8
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     9
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    10
import java.net.URL
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    11
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74962
diff changeset
    13
object Flarum {
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    14
  // see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
74961
bb0858cc574e tuned signature;
wenzelm
parents: 74946
diff changeset
    15
  val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    16
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    17
  def server(url: URL): Server = new Server(url)
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    18
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74962
diff changeset
    19
  class Server private[Flarum](url: URL) extends JSON_API.Service(url) {
76618
aeded421d374 clarified signature: more general operations;
wenzelm
parents: 75393
diff changeset
    20
    def get_api(route: String): JSON_API.Root = get_root(Url.append_path("api", route))
74962
2c9c4ad4c816 clarified signature;
wenzelm
parents: 74961
diff changeset
    21
    val root: JSON_API.Root = get_api("")
2c9c4ad4c816 clarified signature;
wenzelm
parents: 74961
diff changeset
    22
    def users: JSON_API.Root = get_api("users")
2c9c4ad4c816 clarified signature;
wenzelm
parents: 74961
diff changeset
    23
    def groups: JSON_API.Root = get_api("groups")
2c9c4ad4c816 clarified signature;
wenzelm
parents: 74961
diff changeset
    24
    def discussions: JSON_API.Root = get_api("discussions")
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    25
  }
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    26
}