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