src/Pure/General/http.scala
changeset 65088 18f2d388fab4
parent 65087 11e332c4e39f
child 65828 02dd430d80c5
equal deleted inserted replaced
65087:11e332c4e39f 65088:18f2d388fab4
   138   private lazy val html_fonts: SortedMap[String, Bytes] =
   138   private lazy val html_fonts: SortedMap[String, Bytes] =
   139     SortedMap(
   139     SortedMap(
   140       Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
   140       Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
   141 
   141 
   142   def fonts(root: String = "/fonts"): Handler =
   142   def fonts(root: String = "/fonts"): Handler =
   143   {
       
   144     get(root, uri =>
   143     get(root, uri =>
   145       {
   144       {
   146         val uri_name = uri.toString
   145         val uri_name = uri.toString
   147         if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1))))
   146         if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1))))
   148         else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) })
   147         else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) })
   149       })
   148       })
   150   }
       
   151 }
   149 }