diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-05 13:36:16 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-05 13:36:16 +0000 |
| commit | 85e03ea194b95309daed712dccab83a9fba0814a (patch) | |
| tree | 68f14ef8205e92b1b39e91b6db7e7794d48de614 /tools/coqdoc/output.ml | |
| parent | e1c8e5ca2e8cdb03b090b6c049e417f3c7be50f3 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7797 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 7dcba665e..c81bbf7a4 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -61,7 +61,7 @@ let externals = ref true let coqlib = ref "http://coq.inria.fr/library/" let raw_comments = ref false -let charset = ref "" +let charset = ref "iso-8859-1" let inputenc = ref "" let latin1 = ref false let utf8 = ref false @@ -322,29 +322,31 @@ module Html = struct let header () = if !header_trailer then begin + printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n"; + printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n"; printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n"; - if !charset != "" then - printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\">" !charset; - printf "<link rel=\"stylesheet\" href=\"style.css\" type=\"text/css\">"; + printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset; + printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n"; printf "<title>%s</title>\n</head>\n\n" !page_title; - printf "<body>\n\n" + printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n"; + printf "<div id=\"main\">\n\n" end - let self = "http://www.lri.fr/~filliatr/coqdoc/" + let self = "http://coq.inria.fr" let trailer () = if !index && !current_module <> "Index" then - printf "<hr/><a href=\"index.html\">Index</a>"; + printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"index.html\">Index</a>"; if !header_trailer then begin printf "<hr/><font size=\"-1\">This page has been generated by "; printf "<a href=\"%s\">coqdoc</a></font>\n" self; - printf "</body>\n</html>" + printf "</div>\n\n</div>\n\n</body>\n</html>" end let start_module () = if not !short then begin (* add_toc_entry (Toc_library !current_module); *) - printf "<h1>Library %s</h1>\n\n" !current_module + printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module end let indentation n = for i = 1 to n do printf " " done @@ -374,7 +376,7 @@ module Html = struct let stop_verbatim () = printf "</pre>\n" let module_ref m s = - printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" + printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>" (*i match find_module m with | Local -> @@ -388,18 +390,18 @@ module Html = struct let ident_ref m s = match find_module m with | Local -> - printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>" + printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>" | Coqlib when !externals -> let m = Filename.concat !coqlib m in - printf "<a href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>" + printf "<a class=\"idref\" href=\"%s.html#%s\">" m s; raw_ident s; printf "</a>" | Coqlib | Unknown -> raw_ident s let ident s loc = if is_keyword s then begin - printf "<code class=\"keyword\">"; + printf "<span class=\"keyword\">"; raw_ident s; - printf "</code>" + printf "</span>" end else try (match Index.find !current_module loc with @@ -448,11 +450,11 @@ module Html = struct let start_doc () = if not !raw_comments then - printf "\n<table width=\"100%%\"><tr class=\"doc\"><td>\n" + printf "\n<div class=\"doc\">\n" let end_doc () = stop_item (); - if not !raw_comments then printf "\n</td></tr></table>\n" + if not !raw_comments then printf "\n</div>\n" let start_code () = end_doc (); start_coq () @@ -471,7 +473,7 @@ module Html = struct stop_item (); printf "<a name=\"%s\"></a><h%d>" lab lev; f (); - printf "</h%d>\n" lev + printf "</h%d class=\"section\">\n" lev let rule () = printf "<hr/>\n" |