equal
deleted
inserted
replaced
152 else None) |
152 else None) |
153 |
153 |
154 |
154 |
155 /* fonts */ |
155 /* fonts */ |
156 |
156 |
157 private lazy val html_fonts: List[(String, Bytes)] = |
157 private lazy val html_fonts: List[Isabelle_Fonts.Entry] = Isabelle_Fonts.fonts(html = true) |
158 Isabelle_Fonts.fonts(html = true).map(entry => (entry.name -> entry.bytes)) |
|
159 |
158 |
160 def fonts(root: String = "/fonts"): Handler = |
159 def fonts(root: String = "/fonts"): Handler = |
161 get(root, arg => |
160 get(root, arg => |
162 { |
161 { |
163 val uri_name = arg.uri.toString |
162 val uri_name = arg.uri.toString |
164 if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1)))) |
163 if (uri_name == root) { |
165 else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) }) |
164 Some(Response.text(cat_lines(html_fonts.map(entry => entry.path.base_name)))) |
|
165 } |
|
166 else { |
|
167 html_fonts.collectFirst( |
|
168 { case entry if uri_name == root + "/" + entry.path.base_name => Response(entry.bytes) }) |
|
169 } |
166 }) |
170 }) |
167 } |
171 } |