From 98af1982684a02f9521d28594e0fa01ac3275083 Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 28 Mar 2006 17:34:15 +0000 Subject: - correction d'un bug dans coqdoc (multi_index) - modif. de la génération de la doc de stdlib MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/Makefile | 6 ++- doc/stdlib/index-list.html.template | 2 +- tools/coqdoc/main.ml | 8 ++-- tools/coqdoc/output.ml | 89 ++++++++++++++++++++++--------------- tools/coqdoc/output.mli | 1 + 5 files changed, 63 insertions(+), 43 deletions(-) diff --git a/doc/Makefile b/doc/Makefile index d1998d4b1..e0fd8ac7b 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -215,7 +215,7 @@ stdlib/index-body.html: $(GLOBDUMP) - rm -rf stdlib/html mkdir stdlib/html (cd stdlib/html;\ - $(COQDOC) -q --multi-index --body-only --html --glob-from $(GLOBDUMP)\ + $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\ -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v) mv stdlib/html/index.html stdlib/index-body.html @@ -223,7 +223,9 @@ stdlib/index-list.html: stdlib/index-list.html.template COQTOP=$(COQTOP) ./stdlib/make-library-index stdlib/index-list.html stdlib/html/index.html: stdlib/index-list.html stdlib/index-body.html stdlib/index-trailer.html - cat $^ > $@ + cat stdlib/index-list.html > $@ + sed -n -e '//,/<\/table>/p' stdlib/index-body.html >> $@ + cat stdlib/index-trailer.html >> $@ ### Standard library (printable format - produces > 350 pages) diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e86430e38..cbb8580d3 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -1,7 +1,7 @@ - +The Coq Standard Library </head> diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index f81a3b78b..c9860c188 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -60,8 +60,6 @@ let usage () = prerr_endline " --charset <string> set HTML charset"; prerr_endline " --inputenc <string> set LaTeX input encoding"; prerr_endline ""; - prerr_endline - "On-line documentation at http://www.lri.fr/~filliatr/coqdoc/\n"; exit 1 (*s \textbf{Banner.} Always printed. Notice that it is printed on error @@ -365,6 +363,7 @@ let copy src dst = with End_of_file -> close_in cin; close_out cout + (*s Functions for generating output files *) let gen_one_file l = @@ -373,11 +372,11 @@ let gen_one_file l = set_module m; coq_file f m | Latex_file _ -> () in - header (); + if (!header_trailer) then header (); if !toc then make_toc (); List.iter file l; if !index then make_index(); - trailer () + if (!header_trailer) then trailer () let gen_mult_files l = let file = function @@ -394,6 +393,7 @@ let gen_mult_files l = in List.iter file l; if (!index && !target_language=HTML) then begin + if (!multi_index) then make_multi_index (); open_out_file "index.html"; page_title := (if !title <> "" then !title else "Index"); if (!header_trailer) then header (); diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index fcf83a391..ddba3c509 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -255,6 +255,8 @@ module Latex = struct let end_inline_coq () = () + let make_multi_index () = () + let make_index () = () let make_toc () = printf "\\tableofcontents\n" @@ -451,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) = - open_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_out_file () - 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) -> @@ -472,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 -> @@ -481,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) -> @@ -493,34 +484,57 @@ 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 () = - let idxl = + let all_index = let glob,bt = Index.all_entries () in - format_global_index glob :: - List.map format_bytype_index bt + (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 - let navig () = navig_index idxl in current_module := "Index"; - 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 if !title <> "" then printf "<h1>%s</h1>\n" !title; - navig (); - List.iter one_index idxl; - printf "<hr/>"; - navig () - + print_table (); + if not (!multi_index) then + begin + List.iter print_one_index all_index; + printf "<hr/>"; print_table () + end + let make_toc () = let make_toc_entry = function | Toc_library m -> @@ -669,6 +683,8 @@ module TeXmacs = struct let end_inline_coq () = printf "]>" + let make_multi_index () = () + let make_index () = () let make_toc () = () @@ -737,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 diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index f80dca322..824e267e5 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -62,5 +62,6 @@ val stop_latex_math : unit -> unit val start_verbatim : unit -> unit val stop_verbatim : unit -> unit +val make_multi_index : unit -> unit val make_index : unit -> unit val make_toc : unit -> unit -- cgit v1.2.3