src/Pure/Tools/flarum.scala
author wenzelm
Tue, 21 Dec 2021 19:42:20 +0100
changeset 74961 bb0858cc574e
parent 74946 0dd14d8b16da
child 74962 2c9c4ad4c816
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/flarum.scala
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
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    13
object Flarum
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    14
{
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    15
  // see RFC3339 in https://www.php.net/manual/en/class.datetimeinterface.php
74961
bb0858cc574e tuned signature;
wenzelm
parents: 74946
diff changeset
    16
  val Date_Format: Date.Format = Date.Format("uuuu-MM-dd'T'HH:mm:ssxxx")
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    17
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    18
  def server(url: URL): Server = new Server(url)
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    19
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    20
  class Server private[Flarum](url: URL)
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    21
  {
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    22
    override def toString: String = url.toString
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    23
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    24
    def get(route: String): HTTP.Content =
74946
0dd14d8b16da support for JSON:API;
wenzelm
parents: 74945
diff changeset
    25
      HTTP.Client.get(if (route.isEmpty) url else new URL(url, route))
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    26
74946
0dd14d8b16da support for JSON:API;
wenzelm
parents: 74945
diff changeset
    27
    def get_api(route: String = ""): JSON_API.Root =
0dd14d8b16da support for JSON:API;
wenzelm
parents: 74945
diff changeset
    28
      JSON_API.Root(get("api" + (if (route.isEmpty) "" else "/" + route)).json)
0dd14d8b16da support for JSON:API;
wenzelm
parents: 74945
diff changeset
    29
74961
bb0858cc574e tuned signature;
wenzelm
parents: 74946
diff changeset
    30
    val root: JSON_API.Root = get_api()
74945
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    31
  }
4dc90b43ba94 support for Flarum server;
wenzelm
parents:
diff changeset
    32
}