# HG changeset patch
# User wenzelm
# Date 1488468317 -3600
# Node ID 18f2d388fab4716886443e279cbf5d7b3fe95822
# Parent  11e332c4e39f6a021e202e089a36cb7bd77f8eab
tuned;

diff -r 11e332c4e39f -r 18f2d388fab4 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 16:23:39 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 16:25:17 2017 +0100
@@ -140,12 +140,10 @@
       Isabelle_System.fonts(html = true).map(path => (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(html_fonts.map(_._1))))
         else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) })
       })
-  }
 }