equal
deleted
inserted
replaced
135 |
135 |
136 /* fonts */ |
136 /* fonts */ |
137 |
137 |
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_name -> Bytes.read(path))): _*) |
141 |
141 |
142 def fonts(root: String = "/fonts"): Handler = |
142 def fonts(root: String = "/fonts"): Handler = |
143 get(root, uri => |
143 get(root, uri => |
144 { |
144 { |
145 val uri_name = uri.toString |
145 val uri_name = uri.toString |