equal
deleted
inserted
replaced
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 } |