diff options
Diffstat (limited to 'tools/coqdoc/output.ml')
| -rw-r--r-- | tools/coqdoc/output.ml | 212 |
1 files changed, 79 insertions, 133 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index c10f3683..4c4cf5ec 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -6,30 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml,v 1.7.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: output.ml 8669 2006-03-28 17:34:15Z notin $ i*) +open Cdglobals open Index -(*s Target language *) - -type target_language = LaTeX | HTML | TeXmacs - -let target_language = ref HTML - (*s Low level output *) -let out_channel = ref stdout -let output_is_file = ref false -let output_dir = ref "" - -let set_out_file f = - let f = if !output_dir <> "" then Filename.concat !output_dir f else f in - out_channel := open_out f; - output_is_file := true - -let close () = - if !output_is_file then close_out !out_channel - let output_char c = Pervasives.output_char !out_channel c let output_string s = Pervasives.output_string !out_channel s @@ -38,43 +21,6 @@ let printf s = Printf.fprintf !out_channel s let sprintf = Printf.sprintf -let dump_file f = - let ch = open_in f in - try - while true do - Pervasives.output_char !out_channel (input_char ch) - done - with End_of_file -> close_in ch - -(*s Options *) - -let header_trailer = ref true -let quiet = ref false -let light = ref false -let short = ref false -let index = ref true -let multi_index = ref false -let toc = ref false -let page_title = ref "" -let title = ref "" -let externals = ref true -let coqlib = ref "http://coq.inria.fr/library/" -let raw_comments = ref false - -let charset = ref "" -let inputenc = ref "" -let latin1 = ref false -let utf8 = ref false - -let set_latin1 () = - charset := "iso-8859-1"; - inputenc := "latin1"; - latin1 := true - -let set_utf8 () = - charset := "utf-8"; - inputenc := "utf8"; - utf8 := true (*s Coq keywords *) @@ -85,9 +31,9 @@ let build_table l = let is_keyword = build_table - [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; + [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; "CoInductive"; "Defined"; "Definition"; - "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; + "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Immediate"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; @@ -145,6 +91,7 @@ let _ = List.iter "|-", "\\ensuremath{\\vdash}"; "forall", "\\ensuremath{\\forall}"; "exists", "\\ensuremath{\\exists}"; + (* "fun", "\\ensuremath{\\lambda}" ? *) ] (*s Table of contents *) @@ -308,6 +255,8 @@ module Latex = struct let end_inline_coq () = () + let make_multi_index () = () + let make_index () = () let make_toc () = printf "\\tableofcontents\n" @@ -321,29 +270,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 @@ -373,7 +324,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 -> @@ -387,18 +338,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 @@ -447,11 +398,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 () @@ -470,7 +421,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" @@ -502,20 +453,8 @@ module Html = struct let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries - let separate_index navig i = - let idx = i.idx_name in - let one_letter ((c,l) as cl) = - set_out_file (sprintf "index_%s_%c.html" idx c); - header (); - navig (); - printf "<hr/>"; - letter_index true idx cl; - if List.length l > 30 then begin printf "<hr/>"; navig () end; - trailer (); - close () - in - List.iter one_letter i.idx_entries - + (* Construction d'une liste des index (1 index global, puis 1 + index par catégorie) *) let format_global_index = Index.map (fun s (m,t) -> @@ -523,7 +462,7 @@ module Html = struct "[library]", m ^ ".html" else sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (entry_type t) m m , - sprintf "%s.html#%s" m s) + sprintf "%s.html#%s" m s) let format_bytype_index = function | Library, idx -> @@ -532,9 +471,10 @@ module Html = struct Index.map (fun s m -> let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in - (text, sprintf "%s.html#%s" m s)) idx + (text, sprintf "%s.html#%s" m s)) idx - let navig_one_index i = + (* Impression de la table d'index *) + let print_index_table_item i = printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name); List.iter (fun (c,l) -> @@ -544,52 +484,58 @@ module Html = struct printf "<td>%c</td>\n" c) i.idx_entries; let n = i.idx_size in - printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry"); - printf "</tr>\n" + printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry"); + printf "</tr>\n" - let navig_index il = + let print_index_table idxl = printf "<table>\n"; - List.iter navig_one_index il; + List.iter print_index_table_item idxl; printf "</table>\n" - + + let make_one_multi_index prt_tbl i = + (* Attn: make_one_multi_index créé un nouveau fichier... *) + let idx = i.idx_name in + let one_letter ((c,l) as cl) = + open_out_file (sprintf "index_%s_%c.html" idx c); + if (!header_trailer) then header (); + prt_tbl (); printf "<hr/>"; + letter_index true idx cl; + if List.length l > 30 then begin printf "<hr/>"; prt_tbl () end; + if (!header_trailer) then trailer (); + close_out_file () + in + List.iter one_letter i.idx_entries + + let make_multi_index () = + let all_index = + let glob,bt = Index.all_entries () in + (format_global_index glob) :: + (List.map format_bytype_index bt) in + let print_table () = print_index_table all_index in + List.iter (make_one_multi_index print_table) all_index + let make_index () = - if !index then begin - let idxl = - let glob,bt = Index.all_entries () in - format_global_index glob :: - List.map format_bytype_index bt - in - let navig () = navig_index idxl in - set_out_file "index.html"; + let all_index = + let glob,bt = Index.all_entries () in + (format_global_index glob) :: + (List.map format_bytype_index bt) in + let print_table () = print_index_table all_index in + let print_one_index i = + if i.idx_size > 0 then begin + printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name); + all_letters i + end + in current_module := "Index"; - page_title := (if !title <> "" then !title else "Index"); - header (); if !title <> "" then printf "<h1>%s</h1>\n" !title; - navig (); - if !multi_index then begin - trailer (); - close (); - List.iter (separate_index navig) idxl; - end else begin - let one_index i = - if i.idx_size > 0 then begin - printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name); - all_letters i - end - in - List.iter one_index idxl; - printf "<hr/>"; - navig (); - trailer (); - close () - end; - end - + print_table (); + if not (!multi_index) then + begin + List.iter print_one_index all_index; + printf "<hr/>"; print_table () + end + let make_toc () = - set_out_file "toc.html"; - page_title := (if !title <> "" then !title else "Table of contents"); - header (); - if !title <> "" then printf "<h1>%s</h1>\n" !title; let make_toc_entry = function | Toc_library m -> stop_item (); @@ -600,9 +546,6 @@ module Html = struct in Queue.iter make_toc_entry toc_q; stop_item (); - if !index then printf "<a href=\"index.html\"><h2>Index</h2></a>"; - trailer (); - close () end @@ -740,6 +683,8 @@ module TeXmacs = struct let end_inline_coq () = printf "]>" + let make_multi_index () = () + let make_index () = () let make_toc () = () @@ -808,5 +753,6 @@ let verbatim_char = select output_char Html.char TeXmacs.char let hard_verbatim_char = output_char +let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index let make_index = select Latex.make_index Html.make_index TeXmacs.make_index let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc |