# HG changeset patch
# User wenzelm
# Date 1488460241 -3600
# Node ID 8a5c2b86c5f68691010f9d70bb860a8de570ef5c
# Parent  2339994e879096a27396e31a01af5970160f230c
handler for Isabelle fonts;

diff -r 2339994e8790 -r 8a5c2b86c5f6 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) })
+      })
+  }
 }