equal
deleted
inserted
replaced
242 |
242 |
243 |
243 |
244 (* token translations *) |
244 (* token translations *) |
245 |
245 |
246 fun style stl = |
246 fun style stl = |
247 apfst (enclose ("<span class=" ^ quote stl ^ ">") "</span>") o output_width; |
247 apfst (enclose ("<span class=" ^ Library.quote stl ^ ">") "</span>") o output_width; |
248 |
248 |
249 val html_trans = |
249 val html_trans = |
250 [("class", style "tclass"), |
250 [("class", style "tclass"), |
251 ("tfree", style "tfree"), |
251 ("tfree", style "tfree"), |
252 ("tvar", style "tvar"), |
252 ("tvar", style "tvar"), |
271 val file_path = file_name o Url.pack; |
271 val file_path = file_name o Url.pack; |
272 |
272 |
273 |
273 |
274 (* misc *) |
274 (* misc *) |
275 |
275 |
276 fun href_name s txt = "<a href=" ^ quote s ^ ">" ^ txt ^ "</a>"; |
276 fun href_name s txt = "<a href=" ^ Library.quote s ^ ">" ^ txt ^ "</a>"; |
277 fun href_path path txt = href_name (Url.pack path) txt; |
277 fun href_path path txt = href_name (Url.pack path) txt; |
278 |
278 |
279 fun href_opt_name None txt = txt |
279 fun href_opt_name None txt = txt |
280 | href_opt_name (Some s) txt = href_name s txt; |
280 | href_opt_name (Some s) txt = href_name s txt; |
281 |
281 |