18 val href_path: Url.T -> text -> text |
18 val href_path: Url.T -> text -> text |
19 val href_opt_path: Url.T option -> text -> text |
19 val href_opt_path: Url.T option -> text -> text |
20 val para: text -> text |
20 val para: text -> text |
21 val preform: text -> text |
21 val preform: text -> text |
22 val verbatim: string -> text |
22 val verbatim: string -> text |
23 val with_charset: string -> ('a -> 'b) -> 'a -> 'b |
|
24 val begin_document: string -> text |
23 val begin_document: string -> text |
25 val end_document: text |
24 val end_document: text |
26 val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text |
25 val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text |
27 val applet_pages: string -> Url.T * string -> (string * string) list |
26 val applet_pages: string -> Url.T * string -> (string * string) list |
28 val theory_entry: Url.T * string -> text |
27 val theory_entry: Url.T * string -> text |
274 val verbatim = preform o output; |
273 val verbatim = preform o output; |
275 |
274 |
276 |
275 |
277 (* document *) |
276 (* document *) |
278 |
277 |
279 val charset = Unsynchronized.ref "ISO-8859-1"; |
|
280 fun with_charset s = Unsynchronized.setmp charset s; (* FIXME unreliable *) |
|
281 |
|
282 fun begin_document title = |
278 fun begin_document title = |
283 let val cs = ! charset in |
279 "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\ |
284 "<?xml version=\"1.0\" encoding=\"" ^ cs ^ "\" ?>\n\ |
280 \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \ |
285 \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \ |
281 \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\ |
286 \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\ |
282 \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\ |
287 \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\ |
283 \<head>\n\ |
288 \<head>\n\ |
284 \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\ |
289 \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=" ^ cs ^ "\"/>\n\ |
285 \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\ |
290 \<title>" ^ plain (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\ |
286 \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\ |
291 \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\ |
287 \</head>\n\ |
292 \</head>\n\ |
288 \\n\ |
293 \\n\ |
289 \<body>\n\ |
294 \<body>\n\ |
290 \<div class=\"head\">\ |
295 \<div class=\"head\">\ |
291 \<h1>" ^ plain title ^ "</h1>\n"; |
296 \<h1>" ^ plain title ^ "</h1>\n" |
|
297 end; |
|
298 |
292 |
299 val end_document = "\n</div>\n</body>\n</html>\n"; |
293 val end_document = "\n</div>\n</body>\n</html>\n"; |
300 |
294 |
301 fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); |
295 fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); |
302 val up_link = gen_link "Up"; |
296 val up_link = gen_link "Up"; |