src/Pure/Tools/flarum.scala
author wenzelm
Sat, 30 Jul 2022 14:49:22 +0200
changeset 75733 d3430f302c2e
parent 75393 87ebf5a50283
child 76618 aeded421d374
permissions -rw-r--r--
clarified signature;

/*  Title:      Pure/General/flarum.scala
    Author:     Makarius

Support for Flarum forum server: https://flarum.org
*/

package isabelle


import java.net.URL


object Flarum {
  // see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
  val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")

  def server(url: URL): Server = new Server(url)

  class Server private[Flarum](url: URL) extends JSON_API.Service(url) {
    def get_api(route: String): JSON_API.Root =
      get_root("api" + (if (route.isEmpty) "" else "/" + route))

    val root: JSON_API.Root = get_api("")
    def users: JSON_API.Root = get_api("users")
    def groups: JSON_API.Root = get_api("groups")
    def discussions: JSON_API.Root = get_api("discussions")
  }
}