--- 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) })
+ })
+ }
}