support for Flarum server;
authorwenzelm
Wed, 15 Dec 2021 19:41:30 +0100
changeset 74945 4dc90b43ba94
parent 74944 9b14491ca5c6
child 74946 0dd14d8b16da
support for Flarum server;
etc/build.props
src/Pure/General/http.scala
src/Pure/Tools/flarum.scala
--- 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
+  }
+}