handler for Isabelle fonts;
authorwenzelm
Thu, 02 Mar 2017 14:10:41 +0100
changeset 65079 8a5c2b86c5f6
parent 65078 2339994e8790
child 65080 2b6ed26b7597
handler for Isabelle fonts;
src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 13:36:07 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 14:10:41 2017 +0100
@@ -10,6 +10,8 @@
 import java.net.{InetAddress, InetSocketAddress, URI}
 import com.sun.net.httpserver.{HttpExchange, HttpHandler, HttpServer}
 
+import scala.collection.immutable.SortedMap
+
 
 object HTTP
 {
@@ -100,4 +102,26 @@
     for (handler <- handlers) server += handler
     server
   }
+
+
+  /* Isabelle resources */
+
+  private lazy val isabelle_fonts: SortedMap[String, Bytes] =
+    SortedMap(
+      (for {
+        variable <- List("ISABELLE_FONTS", "ISABELLE_FONTS_HTML")
+        path <- Path.split(Isabelle_System.getenv_strict(variable))
+      } yield (path.base.implode -> Bytes.read(path))): _*)
+
+  def fonts(root: String = "/fonts"): Handler =
+  {
+    get(root, uri =>
+      {
+        val uri_name = uri.toString
+        if (uri_name == root) Some(Response.text(cat_lines(isabelle_fonts.map(_._1))))
+        else
+          isabelle_fonts.collectFirst(
+            { case (name, file) if uri_name == root + "/" + name => Response(file) })
+      })
+  }
 }