--- a/etc/build.props Wed Dec 15 19:39:02 2021 +0100
+++ b/etc/build.props Wed Dec 15 19:41:30 2021 +0100
@@ -170,6 +170,7 @@
src/Pure/Tools/debugger.scala \
src/Pure/Tools/doc.scala \
src/Pure/Tools/dump.scala \
+ src/Pure/Tools/flarum.scala \
src/Pure/Tools/fontforge.scala \
src/Pure/Tools/java_monitor.scala \
src/Pure/Tools/logo.scala \
--- a/src/Pure/General/http.scala Wed Dec 15 19:39:02 2021 +0100
+++ b/src/Pure/General/http.scala Wed Dec 15 19:41:30 2021 +0100
@@ -31,6 +31,7 @@
elapsed_time: Time = Time.zero)
{
def text: String = new String(bytes.array, encoding)
+ def json: JSON.T = JSON.parse(text)
}
def read_content(file: JFile): Content =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/flarum.scala Wed Dec 15 19:41:30 2021 +0100
@@ -0,0 +1,29 @@
+/* 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("uuuu-MM-dd'T'HH:mm:ssxxx")
+
+ def server(url: URL): Server = new Server(url)
+
+ class Server private[Flarum](url: URL)
+ {
+ override def toString: String = url.toString
+
+ def get(route: String): HTTP.Content =
+ HTTP.Client.get(new URL(url, route))
+
+ val api: JSON.T = get("api").json
+ }
+}