From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tools/coqdoc/alpha.ml | 45 +++ tools/coqdoc/alpha.mli | 19 ++ tools/coqdoc/coqdoc.sty | 58 ++++ tools/coqdoc/index.mli | 59 ++++ tools/coqdoc/index.mll | 327 +++++++++++++++++++ tools/coqdoc/main.ml | 420 +++++++++++++++++++++++++ tools/coqdoc/output.ml | 812 ++++++++++++++++++++++++++++++++++++++++++++++++ tools/coqdoc/output.mli | 92 ++++++ tools/coqdoc/pretty.mli | 19 ++ tools/coqdoc/pretty.mll | 586 ++++++++++++++++++++++++++++++++++ tools/coqdoc/style.css | 23 ++ 11 files changed, 2460 insertions(+) create mode 100644 tools/coqdoc/alpha.ml create mode 100644 tools/coqdoc/alpha.mli create mode 100644 tools/coqdoc/coqdoc.sty create mode 100644 tools/coqdoc/index.mli create mode 100644 tools/coqdoc/index.mll create mode 100644 tools/coqdoc/main.ml create mode 100644 tools/coqdoc/output.ml create mode 100644 tools/coqdoc/output.mli create mode 100644 tools/coqdoc/pretty.mli create mode 100644 tools/coqdoc/pretty.mll create mode 100644 tools/coqdoc/style.css (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml new file mode 100644 index 00000000..2418b6e1 --- /dev/null +++ b/tools/coqdoc/alpha.ml @@ -0,0 +1,45 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'A' + | '\199' -> 'C' + | '\200'..'\203' -> 'E' + | '\204'..'\207' -> 'I' + | '\209' -> 'N' + | '\210'..'\214' -> 'O' + | '\217'..'\220' -> 'U' + | '\221' -> 'Y' + | c -> c + +let norm_string s = + let u = String.copy s in + for i = 0 to String.length s - 1 do + u.[i] <- norm_char s.[i] + done; + u + +let compare_char c1 c2 = match norm_char c1, norm_char c2 with + | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2 + | 'A'..'Z', _ -> -1 + | _, 'A'..'Z' -> 1 + | c1, c2 -> compare c1 c2 + +let compare_string s1 s2 = + let n1 = String.length s1 in + let n2 = String.length s2 in + let rec cmp i = + if i == n1 || i == n2 then + n1 - n2 + else + let c = compare_char s1.[i] s2.[i] in + if c == 0 then cmp (succ i) else c + in + cmp 0 diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli new file mode 100644 index 00000000..46409c9a --- /dev/null +++ b/tools/coqdoc/alpha.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* char -> int +val compare_string : string -> string -> int + +(* Alphabetic normalization. *) + +val norm_char : char -> char +val norm_string : string -> string diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty new file mode 100644 index 00000000..7f7aa9aa --- /dev/null +++ b/tools/coqdoc/coqdoc.sty @@ -0,0 +1,58 @@ + +% This is coqdoc.sty, by Jean-Christophe Filliātre +% This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc) +% +% You can modify the following macros to customize the appearance +% of the document. + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{coqdoc}[2002/02/11] + +% Headings + +\usepackage{fancyhdr} +\newcommand{\coqdocleftpageheader}{\thepage\ -- \today} +\newcommand{\coqdocrightpageheader}{\today\ -- \thepage} +\pagestyle{fancyplain} + +%BEGIN LATEX +\plainheadrulewidth 0.4pt +\plainfootrulewidth 0pt +\lhead[\coqdocleftpageheader]{\leftmark} +\rhead[\leftmark]{\coqdocrightpageheader} +\cfoot{} +%END LATEX + +% Hevea puts to much space with \medskip and \bigskip +%HEVEA\renewcommand{\medskip}{} +%HEVEA\renewcommand{\bigskip}{} + +% own name +\newcommand{\coqdoc}{\textsf{coqdoc}} + +% pretty underscores (the package fontenc causes ugly underscores) +%BEGIN LATEX +\def\_{\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em} +%END LATEX + +% macro for typesetting keywords +\newcommand{\coqdockw}[1]{\textsf{#1}} + +% macro for typesetting identifiers +\newcommand{\coqdocid}[1]{\textit{#1}} + +% newline and indentation +%BEGIN LATEX +\newcommand{\coqdoceol}{\setlength\parskip{0pt}\par} +\newcommand{\coqdocindent}[1]{\noindent\kern#1} +%END LATEX +%HEVEA\newcommand{\coqdoceol}{\begin{rawhtml}
\end{rawhtml}} +%HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}} + +% macro for typesetting the title of a module implementation +\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{}} + +%HEVEA\newcommand{\lnot}{\coqwkw{not}} +%HEVEA\newcommand{\lor}{\coqwkw{or}} +%HEVEA\newcommand{\land}{\&} + diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli new file mode 100644 index 00000000..60c21387 --- /dev/null +++ b/tools/coqdoc/index.mli @@ -0,0 +1,59 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* loc -> index_entry + +val add_module : coq_module -> unit + +type module_kind = Local | Coqlib | Unknown + +val find_module : coq_module -> module_kind + +(*s Scan identifiers introductions from a file *) + +val scan_file : string -> coq_module -> unit + +(*s Read globalizations from a file (produced by coqc -dump-glob) *) + +val read_glob : string -> unit + +(*s Indexes *) + +type 'a index = { + idx_name : string; + idx_entries : (char * (string * 'a) list) list; + idx_size : int } + +val all_entries : unit -> + (coq_module * entry_type) index * + (entry_type * coq_module index) list + +val map : (string -> 'a -> 'b) -> 'a index -> 'b index + diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll new file mode 100644 index 00000000..799825ad --- /dev/null +++ b/tools/coqdoc/index.mll @@ -0,0 +1,327 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + "", s + +let modules = Hashtbl.create 97 +let local_modules = Hashtbl.create 97 + +let add_module m = + let _,id = split_sp m in + Hashtbl.add modules id m; + Hashtbl.add local_modules m () + +type module_kind = Local | Coqlib | Unknown + +let coq_module m = + String.length m >= 4 && String.sub m 0 4 = "Coq." + +let find_module m = + if Hashtbl.mem local_modules m then + Local + else if coq_module m then + Coqlib + else + Unknown + +let ref_module loc s = + try + let n = String.length s in + let i = String.rindex s ' ' in + let id = String.sub s (i+1) (n-i-1) in + add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id + with Not_found -> + () + +(* Building indexes *) + +type 'a index = { + idx_name : string; + idx_entries : (char * (string * 'a) list) list; + idx_size : int } + +let map f i = + { i with idx_entries = + List.map + (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l)) + i.idx_entries } + +let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2 + +let sort_entries el = + let t = Hashtbl.create 97 in + List.iter + (fun c -> Hashtbl.add t c []) + ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; + 'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_']; + List.iter + (fun ((s,_) as e) -> + let c = Alpha.norm_char s.[0] in + let l = try Hashtbl.find t c with Not_found -> [] in + Hashtbl.replace t c (e :: l)) + el; + let res = ref [] in + Hashtbl.iter + (fun c l -> res := (c, List.sort compare_entries l) :: !res) t; + List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res + +let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0 + +let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h [] + +let type_name = function + | Library -> "library" + | Module -> "module" + | Definition -> "definition" + | Inductive -> "inductive" + | Constructor -> "constructor" + | Lemma -> "lemma" + | Variable -> "variable" + | Axiom -> "axiom" + | TacticDefinition -> "tactic" + +let all_entries () = + let gl = ref [] in + let add_g s m t = gl := (s,(m,t)) :: !gl in + let bt = Hashtbl.create 11 in + let add_bt t s m = + let l = try Hashtbl.find bt t with Not_found -> [] in + Hashtbl.replace bt t ((s,m) :: l) + in + let classify (m,_) e = match e with + | Def (s,t) -> add_g s m t; add_bt t s m + | Ref _ | Mod _ -> () + in + Hashtbl.iter classify table; + Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; + { idx_name = "global"; + idx_entries = sort_entries !gl; + idx_size = List.length !gl }, + Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; + idx_entries = sort_entries e; + idx_size = List.length e }) :: l) bt [] + +} + +(*s Shortcuts for regular expressions. *) + +let space = + [' ' '\010' '\013' '\009' '\012'] +let firstchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'] +let identchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' + '\'' '0'-'9'] +let ident = + firstchar identchar* + +let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" +let end_hide = "(*" space* "end" space+ "hide" space* "*)" + +(*s Indexing entry point. *) + +rule traverse = parse + | "Definition" space + { current_type := Definition; index_ident lexbuf; traverse lexbuf } + | "Tactic" space+ "Definition" space + { current_type := TacticDefinition; index_ident lexbuf; traverse lexbuf } + | ("Axiom" | "Parameter") space + { current_type := Axiom; index_ident lexbuf; traverse lexbuf } + | "Fixpoint" space + { current_type := Definition; index_ident lexbuf; fixpoint lexbuf; + traverse lexbuf } + | ("Lemma" | "Theorem") space + { current_type := Lemma; index_ident lexbuf; traverse lexbuf } + | "Inductive" space + { current_type := Inductive; + index_ident lexbuf; inductive lexbuf; traverse lexbuf } + | "Record" space + { current_type := Inductive; index_ident lexbuf; traverse lexbuf } + | "Module" (space+ "Type")? space + { current_type := Module; index_ident lexbuf; traverse lexbuf } +(*i*** + | "Variable" 's'? space + { current_type := Variable; index_idents lexbuf; traverse lexbuf } +***i*) + | "Require" (space+ "Export")? space+ ident + { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf } + | begin_hide + { skip_hide lexbuf; traverse lexbuf } + | "(*" + { comment lexbuf; traverse lexbuf } + | '"' + { string lexbuf; traverse lexbuf } + | eof + { () } + | _ + { traverse lexbuf } + +(*s Index one identifier. *) + +and index_ident = parse + | space+ + { index_ident lexbuf } + | ident + { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) } + | eof + { () } + | _ + { () } + +(*s Index identifiers separated by blanks and/or commas. *) + +and index_idents = parse + | space+ | ',' + { index_idents lexbuf } + | ident + { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf); + index_idents lexbuf } + | eof + { () } + | _ + { skip_until_point lexbuf } + +(*s Index identifiers in an inductive definition (types and constructors). *) + +and inductive = parse + | '|' | ":=" space* '|'? + { current_type := Constructor; index_ident lexbuf; inductive lexbuf } + | "with" space + { current_type := Inductive; index_ident lexbuf; inductive lexbuf } + | '.' + { () } + | eof + { () } + | _ + { inductive lexbuf } + +(*s Index identifiers in a Fixpoint declaration. *) + +and fixpoint = parse + | "with" space + { index_ident lexbuf; fixpoint lexbuf } + | '.' + { () } + | eof + { () } + | _ + { fixpoint lexbuf } + +(*s Skip a possibly nested comment. *) + +and comment = parse + | "*)" { () } + | "(*" { comment lexbuf; comment lexbuf } + | '"' { string lexbuf; comment lexbuf } + | eof { eprintf " *** Unterminated comment while indexing" } + | _ { comment lexbuf } + +(*s Skip a constant string. *) + +and string = parse + | '"' { () } + | eof { eprintf " *** Unterminated string while indexing" } + | _ { string lexbuf } + +(*s Skip everything until the next dot. *) + +and skip_until_point = parse + | '.' { () } + | eof { () } + | _ { skip_until_point lexbuf } + +(*s Skip everything until [(* end hide *)] *) + +and skip_hide = parse + | eof | end_hide { () } + | _ { skip_hide lexbuf } + +{ + + let read_glob f = + let c = open_in f in + let cur_mod = ref "" in + try + while true do + let s = input_line c in + let n = String.length s in + if n > 0 then begin + match s.[0] with + | 'F' -> + cur_mod := String.sub s 1 (n - 1) + | 'R' -> + (try + let i = String.index s ' ' in + let loc = int_of_string (String.sub s 1 (i - 1)) in + let sp = String.sub s (i + 1) (n - i - 1) in + let m',id = split_sp sp in + add_ref !cur_mod loc m' id + with Not_found -> + ()) + | _ -> () + end + done + with End_of_file -> + close_in c + + let scan_file f m = + current_module := m; + let c = open_in f in + let lb = from_channel c in + traverse lb; + close_in c +} diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml new file mode 100644 index 00000000..66d2a993 --- /dev/null +++ b/tools/coqdoc/main.ml @@ -0,0 +1,420 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* on 9 & 10 Mar 2004: + * - handling of absolute filenames (function coq_module) + * - coq_module: chop ./// (arbitrary amount of slashes), not only "./" + * - function chop_prefix not useful anymore. Deleted. + * - correct typo in usage message: "-R" -> "--R" + * - shorten the definition of make_path + * This notice is made to comply with section 2.a of the GPLv2. + * It may be removed or abbreviated as far as I am concerned. + *) + +open Filename +open Printf +open Output +open Pretty + +(*s \textbf{Usage.} Printed on error output. *) + +let usage () = + prerr_endline ""; + prerr_endline "Usage: coqdoc "; + prerr_endline " --html produce a HTML document (default)"; + prerr_endline " --latex produce a LaTeX document"; + prerr_endline " --texmacs produce a TeXmacs document"; + prerr_endline " --dvi output the DVI"; + prerr_endline " --ps output the PostScript"; + prerr_endline " -o write output in file "; + prerr_endline " -d output files into directory "; + prerr_endline " -g (gallina) skip proofs"; + prerr_endline " -s (short) no titles for files"; + prerr_endline " -l light mode (only defs and statements)"; + prerr_endline " -t give a title to the document"; + prerr_endline " --body-only suppress LaTeX/HTML header and trailer"; + prerr_endline " --no-index do not output the index"; + prerr_endline " --multi-index index split in multiple files"; + prerr_endline " --toc output a table of contents"; + prerr_endline " --vernac consider as a .v file"; + prerr_endline " --tex consider as a .tex file"; + prerr_endline " -p insert in LaTeX preamble"; + prerr_endline " --files-from read file names to process in "; + prerr_endline " --quiet quiet mode"; + prerr_endline " --glob-from read Coq globalizations from file "; + prerr_endline " --no-externals no links to Coq standard library"; + prerr_endline " --coqlib set URL for Coq standard library"; + prerr_endline " (default is http://coq.inria.fr/library/)"; + prerr_endline " -R map physical dir to Coq dir"; + prerr_endline " --latin1 set ISO-8859-1 input language"; + prerr_endline " --utf8 set UTF-8 input language"; + prerr_endline " --charset set HTML charset"; + prerr_endline " --inputenc 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 + output, so that when the output of [coqdoc] is redirected this header + is not (unless both standard and error outputs are redirected, of + course). *) + +let banner () = + eprintf "This is coqdoc version %s, compiled on %s\n" + Coq_config.version Coq_config.compile_date; + flush stderr + + +(*s \textbf{Separation of files.} Files given on the command line are + separated according to their type, which is determined by their + suffix. Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\ + files have suffix \verb!.tex!. *) + +let check_if_file_exists f = + if not (Sys.file_exists f) then begin + eprintf "\ncoqdoc: %s: no such file\n" f; + exit 1 + end + +let paths = ref [] + +let add_path m l = paths := (m,l) :: !paths + +let exists_dir dir = + try let _ = Unix.opendir dir in true with Unix.Unix_error _ -> false + +let add_rec_path f l = + let rec traverse abs rel = + add_path abs rel; + let dirh = Unix.opendir abs in + try + while true do + let f = Unix.readdir dirh in + if f <> "" && f.[0] <> '.' && f <> "CVS" then + let abs' = Filename.concat abs f in + try + if exists_dir abs' then traverse abs' (rel ^ "." ^ f) + with Unix.Unix_error _ -> + () + done + with End_of_file -> + Unix.closedir dirh + in + if exists_dir f then traverse f l + +(* turn A/B/C into A.B.C *) +let make_path = Str.global_replace (Str.regexp "/") ".";; + +let coq_module file = +(* TODO + * LEM: + * We should also remove things like "/./" in the middle of the filename, + * rewrite "/foo/../bar" to "/bar", recognise different paths that lead + * to the same file / directory (via symlinks), etc. The best way to do + * all this would be to use the libc function realpath() on _both_ p and + * file / f before comparing them. + * + * The semantics of realpath() on file symlinks might not be what we + * want... (But it is what we want on directory symlinks.) So, we would + * have to cook up our own version of realpath()? + * + * Do all target platforms have realpath()? + *) + let f = chop_extension file in + (* remove leading ./ and any number of slashes after *) + let f = Str.replace_first (Str.regexp "^\\./+") "" f in + if (Str.string_before f 1) = "/" then + (* f is an absolute path. Prefixes must be matched with the beginning of f, + * not prepended + *) + let rec trypath = function + | [] -> make_path f + | (p, lg) :: r -> + (* make sure p ends with a single '/' + * This guarantees that we don't match a file whose name is + * of the form p ^ "foo". It means we may miss p itself, + * but this does not matter: coqdoc doesn't do anything + * of a directory anyway. *) + let p = (Str.replace_first (Str.regexp "/*$") "/" p) in + let p_quoted = (Str.quote p) in + if (Str.string_match (Str.regexp p_quoted) f 0) then + make_path (Filename.concat lg (Str.replace_first (Str.regexp (p_quoted ^ "/*")) "" f)) + else + trypath r + in trypath !paths + else (* f is a relative path *) + let rec trypath = function + | [] -> + make_path f + | (p,lg) :: r -> + let p_file = Filename.concat p file in + if Sys.file_exists p_file then + make_path (Filename.concat lg f) + else + trypath r + in trypath !paths;; + +let what_file f = + check_if_file_exists f; + if check_suffix f ".v" || check_suffix f ".g" then + Vernac_file (f, coq_module f) + else if check_suffix f ".tex" then + Latex_file f + else begin + eprintf "\ncoqdoc: don't know what to do with %s\n" f; + exit 1 + end + +(*s \textbf{Reading file names from a file.} + File names may be given + in a file instead of being given on the command + line. [(files_from_file f)] returns the list of file names contained + in the file named [f]. These file names must be separated by spaces, + tabulations or newlines. + *) + +let files_from_file f = + let files_from_channel ch = + let buf = Buffer.create 80 in + let l = ref [] in + try + while true do + match input_char ch with + | ' ' | '\t' | '\n' -> + if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l; + Buffer.clear buf + | c -> + Buffer.add_char buf c + done; [] + with End_of_file -> + List.rev !l + in + try + check_if_file_exists f; + let ch = open_in f in + let l = files_from_channel ch in + close_in ch;l + with Sys_error s -> begin + eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s; + exit 1 + end + +(*s \textbf{Parsing of the command line.} *) + +let output_file = ref "" +let dvi = ref false +let ps = ref false + +let parse () = + let files = ref [] in + let add_file f = files := f :: !files in + let rec parse_rec = function + | [] -> () + + | ("-nopreamble" | "--nopreamble" | "--no-preamble" + | "-bodyonly" | "--bodyonly" | "--body-only") :: rem -> + header_trailer := false; parse_rec rem + | ("-p" | "--preamble") :: s :: rem -> + push_in_preamble s; parse_rec rem + | ("-p" | "--preamble") :: [] -> + usage () + | ("-noindex" | "--noindex" | "--no-index") :: rem -> + index := false; parse_rec rem + | ("-multi-index" | "--multi-index") :: rem -> + multi_index := true; parse_rec rem + | ("-toc" | "--toc" | "--table-of-contents") :: rem -> + toc := true; parse_rec rem + | ("-o" | "--output") :: f :: rem -> + output_file := f; parse_rec rem + | ("-o" | "--output") :: [] -> + usage () + | ("-d" | "--directory") :: dir :: rem -> + output_dir := dir; parse_rec rem + | ("-d" | "--directory") :: [] -> + usage () + | ("-s" | "--short") :: rem -> + short := true; parse_rec rem + | ("-l" | "-light" | "--light") :: rem -> + gallina := true; light := true; parse_rec rem + | ("-g" | "-gallina" | "--gallina") :: rem -> + gallina := true; parse_rec rem + | ("-t" | "-title" | "--title") :: s :: rem -> + title := s; parse_rec rem + | ("-t" | "-title" | "--title") :: [] -> + usage () + | ("-latex" | "--latex") :: rem -> + Output.target_language := LaTeX; parse_rec rem + | ("-dvi" | "--dvi") :: rem -> + Output.target_language := LaTeX; dvi := true; parse_rec rem + | ("-ps" | "--ps") :: rem -> + Output.target_language := LaTeX; ps := true; parse_rec rem + | ("-html" | "--html") :: rem -> + Output.target_language := HTML; parse_rec rem + | ("-texmacs" | "--texmacs") :: rem -> + Output.target_language := TeXmacs; parse_rec rem + + | ("-charset" | "--charset") :: s :: rem -> + Output.charset := s; parse_rec rem + | ("-charset" | "--charset") :: [] -> + usage () + | ("-inputenc" | "--inputenc") :: s :: rem -> + Output.inputenc := s; parse_rec rem + | ("-inputenc" | "--inputenc") :: [] -> + usage () + | ("-raw-comments" | "--raw-comments") :: rem -> + Output.raw_comments := true; parse_rec rem + | ("-latin1" | "--latin1") :: rem -> + Output.set_latin1 (); parse_rec rem + | ("-utf8" | "--utf8") :: rem -> + Output.set_utf8 (); parse_rec rem + + | ("-q" | "-quiet" | "--quiet") :: rem -> + quiet := true; parse_rec rem + + | ("-h" | "-help" | "-?" | "--help") :: rem -> + banner (); usage () + | ("-v" | "-version" | "--version") :: _ -> + banner (); exit 0 + + | ("-vernac-file" | "--vernac-file") :: f :: rem -> + check_if_file_exists f; + add_file (Vernac_file (f, coq_module f)); parse_rec rem + | ("-vernac-file" | "--vernac-file") :: [] -> + usage () + | ("-tex-file" | "--tex-file") :: f :: rem -> + add_file (Latex_file f); parse_rec rem + | ("-tex-file" | "--tex-file") :: [] -> + usage () + | ("-files" | "--files" | "--files-from") :: f :: rem -> + List.iter (fun f -> add_file (what_file f)) (files_from_file f); + parse_rec rem + | ("-files" | "--files") :: [] -> + usage () + + | "-R" :: path :: log :: rem -> + add_path path log; parse_rec rem + | "-R" :: ([] | [_]) -> + usage () + | ("-glob-from" | "--glob-from") :: f :: rem -> + Index.read_glob f; parse_rec rem + | ("-glob-from" | "--glob-from") :: [] -> + usage () + | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> + Output.externals := false; parse_rec rem + | ("--coqlib" | "-coqlib") :: u :: rem -> + Output.coqlib := u; parse_rec rem + | ("--coqlib" | "-coqlib") :: [] -> + usage () + + | f :: rem -> + add_file (what_file f); parse_rec rem + in + parse_rec (List.tl (Array.to_list Sys.argv)); + List.rev !files + + +(*s The following function produces the output. The default output is + the \LaTeX\ document: in that case, we just call [Web.produce_document]. + If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then + we make calls to \verb!latex! or \verb!dvips! accordingly. *) + +let locally dir f x = + let cwd = Sys.getcwd () in + try + Sys.chdir dir; let y = f x in Sys.chdir cwd; y + with e -> + Sys.chdir cwd; raise e + +let clean_temp_files basefile = + let remove f = try Sys.remove f with _ -> () in + remove (basefile ^ ".tex"); + remove (basefile ^ ".log"); + remove (basefile ^ ".aux"); + remove (basefile ^ ".dvi"); + remove (basefile ^ ".ps"); + remove (basefile ^ ".haux"); + remove (basefile ^ ".html") + +let clean_and_exit file res = clean_temp_files file; exit res + +let cat file = + let c = open_in file in + try + while true do print_char (input_char c) done + with End_of_file -> + close_in c + +let copy src dst = + let cin = open_in src + and cout = open_out dst in + try + while true do Pervasives.output_char cout (input_char cin) done + with End_of_file -> + close_in cin; close_out cout + +let produce_output fl = + if not (!dvi || !ps) then begin + if !output_file <> "" then set_out_file !output_file; + produce_document fl + end else begin + let texfile = temp_file "coqdoc" ".tex" in + let basefile = chop_suffix texfile ".tex" in + set_out_file texfile; + produce_document fl; + let command = + let file = basename texfile in + let file = + if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file + in + sprintf "(latex %s && latex %s) 1>&2 %s" file file + (if !quiet then "> /dev/null" else "") + in + let res = locally (dirname texfile) Sys.command command in + if res <> 0 then begin + eprintf "Couldn't run LaTeX successfully\n"; + clean_and_exit basefile res + end; + let dvifile = basefile ^ ".dvi" in + if !dvi then begin + if !output_file <> "" then + (* we cannot use Sys.rename accross file systems *) + copy dvifile !output_file + else + cat dvifile + end; + if !ps then begin + let psfile = + if !output_file <> "" then !output_file else basefile ^ ".ps" + in + let command = + sprintf "dvips %s -o %s %s" dvifile psfile + (if !quiet then "> /dev/null 2>&1" else "") + in + let res = Sys.command command in + if res <> 0 then begin + eprintf "Couldn't run dvips successfully\n"; + clean_and_exit basefile res + end; + if !output_file = "" then cat psfile + end; + clean_temp_files basefile + end + + +(*s \textbf{Main program.} Print the banner, parse the command line, + read the files and then call [produce_document] from module [Web]. *) + +let main () = + let files = parse () in + if not !quiet then banner (); + if List.length files > 0 then produce_output files + +let _ = Printexc.catch main () diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml new file mode 100644 index 00000000..c10f3683 --- /dev/null +++ b/tools/coqdoc/output.ml @@ -0,0 +1,812 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "" 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 + +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 *) + +let build_table l = + let h = Hashtbl.create 101 in + List.iter (fun key ->Hashtbl.add h key ()) l; + function s -> try Hashtbl.find h s; true with Not_found -> false + +let is_keyword = + build_table + [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; + "CoInductive"; "Defined"; "Definition"; + "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; + "Hypothesis"; "Hypotheses"; + "Immediate"; "Implicit"; "Import"; "Inductive"; + "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; + "Module"; "Module Type"; "Declare Module"; + "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; + "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; + "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; + "Unset"; "Variable"; "Variables"; + "Notation"; + (*i (* correctness *) + "array"; "assert"; "begin"; "do"; "done"; "else"; "end"; "if"; + "in"; "invariant"; "let"; "of"; "ref"; "state"; "then"; "variant"; + "while"; i*) + (*i (* coq terms *) + "with"; "Case"; "Cases"; "Prop"; "Set"; "Type"; i*) + ] + +(*s Current Coq module *) + +let current_module = ref "" + +let set_module m = current_module := m; page_title := m + +(*s Common to both LaTeX and HTML *) + +let item_level = ref 0 + +(*s Customized pretty-print *) + +let token_pp = Hashtbl.create 97 + +let add_printing_token = Hashtbl.replace token_pp + +let find_printing_token tok = + try Hashtbl.find token_pp tok with Not_found -> None, None + +let remove_printing_token = Hashtbl.remove token_pp + +(* predefined pretty-prints *) +let _ = List.iter + (fun (s,l) -> Hashtbl.add token_pp s (Some l, None)) + [ "*" , "\\ensuremath{\\times}"; + "->", "\\ensuremath{\\rightarrow}"; + "->~", "\\ensuremath{\\rightarrow\\lnot}"; + "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; + "<-", "\\ensuremath{\\leftarrow}"; + "<->", "\\ensuremath{\\leftrightarrow}"; + "=>", "\\ensuremath{\\Rightarrow}"; + "<=", "\\ensuremath{\\le}"; + ">=", "\\ensuremath{\\ge}"; + "<>", "\\ensuremath{\\not=}"; + "~", "\\ensuremath{\\lnot}"; + "/\\", "\\ensuremath{\\land}"; + "\\/", "\\ensuremath{\\lor}"; + "|-", "\\ensuremath{\\vdash}"; + "forall", "\\ensuremath{\\forall}"; + "exists", "\\ensuremath{\\exists}"; + ] + +(*s Table of contents *) + +type toc_entry = + | Toc_library of string + | Toc_section of int * (unit -> unit) * string + +let (toc_q : toc_entry Queue.t) = Queue.create () + +let add_toc_entry e = Queue.add e toc_q + +let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r + +(*s LaTeX output *) + +module Latex = struct + + (*s Latex preamble *) + + let (preamble : string Queue.t) = Queue.create () + + let push_in_preamble s = Queue.add s preamble + + let header () = + if !header_trailer then begin + printf "\\documentclass[12pt]{article}\n"; + if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; + printf "\\usepackage[T1]{fontenc}\n"; + printf "\\usepackage{fullpage}\n"; + printf "\\usepackage{coqdoc}\n"; + Queue.iter (fun s -> printf "%s\n" s) preamble; + printf "\\begin{document}\n" + end; + output_string + "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"; + output_string + "%% This file has been automatically generated with the command\n"; + output_string "%% "; + Array.iter (fun s -> printf "%s " s) Sys.argv; + printf "\n"; + output_string + "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n" + + let trailer () = + if !header_trailer then begin + printf "\\end{document}\n" + end + + let char c = match c with + | '\\' -> + printf "\\symbol{92}" + | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> + output_char '\\'; output_char c + | '^' | '~' -> + output_char '\\'; output_char c; printf "{}" + | _ -> + output_char c + + let latex_char = output_char + let latex_string = output_string + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = + if not !short then begin + printf "\\coqdocmodule{"; + raw_ident !current_module; + printf "}\n\n" + end + + let start_latex_math () = output_char '$' + + let stop_latex_math () = output_char '$' + + let start_verbatim () = printf "\\begin{verbatim}" + + let stop_verbatim () = printf "\\end{verbatim}\n" + + let indentation n = + if n == 0 then + printf "\\noindent\n" + else + let space = 0.5 *. (float n) in + printf "\\coqdocindent{%2.2fem}\n" space + + let with_latex_printing f tok = + try + (match Hashtbl.find token_pp tok with + | Some s, _ -> output_string s + | _ -> f tok) + with Not_found -> + f tok + + let ident s _ = + if is_keyword s then begin + printf "\\coqdockw{"; raw_ident s; printf "}" + end else begin + printf "\\coqdocid{"; raw_ident s; printf "}" + end + + let ident s l = with_latex_printing (fun s -> ident s l) s + + let symbol = with_latex_printing raw_ident + + let rec reach_item_level n = + if !item_level < n then begin + printf "\n\\begin{itemize}\n\\item "; incr item_level; + reach_item_level n + end else if !item_level > n then begin + printf "\n\\end{itemize}\n"; decr item_level; + reach_item_level n + end + + let item n = + let old_level = !item_level in + reach_item_level n; + if n <= old_level then printf "\n\\item " + + let stop_item () = reach_item_level 0 + + let start_doc () = printf "\n\n\n\\noindent\n" + + let end_doc () = stop_item (); printf "\n\n\n" + + let start_coq () = () + + let end_coq () = () + + let start_code () = end_doc (); start_coq () + + let end_code () = end_coq (); start_doc () + + let section_kind = function + | 1 -> "\\section{" + | 2 -> "\\subsection{" + | 3 -> "\\subsubsection{" + | 4 -> "\\paragraph{" + | _ -> assert false + + let section lev f = + stop_item (); + output_string (section_kind lev); + f (); + printf "}\n\n" + + let rule () = + printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" + + let paragraph () = stop_item (); printf "\n\n\\medskip\n" + + let line_break () = printf "\\coqdoceol\n" + + let empty_line_of_code () = printf "\n\n\\medskip\n" + + let start_inline_coq () = () + + let end_inline_coq () = () + + let make_index () = () + + let make_toc () = printf "\\tableofcontents\n" + +end + + +(*s HTML output *) + +module Html = struct + + let header () = + if !header_trailer then begin + printf "\n\n"; + if !charset != "" then + printf "" !charset; + printf ""; + printf "%s\n\n\n" !page_title; + printf "\n\n" + end + + let self = "http://www.lri.fr/~filliatr/coqdoc/" + + let trailer () = + if !index && !current_module <> "Index" then + printf "
Index"; + if !header_trailer then begin + printf "
This page has been generated by "; + printf "coqdoc\n" self; + printf "\n" + end + + let start_module () = + if not !short then begin + (* add_toc_entry (Toc_library !current_module); *) + printf "

Library %s

\n\n" !current_module + end + + let indentation n = for i = 1 to n do printf " " done + + let line_break () = printf "
\n" + + let empty_line_of_code () = printf "\n
\n" + + let char = function + | '<' -> printf "<" + | '>' -> printf ">" + | '&' -> printf "&" + | c -> output_char c + + let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + + let latex_char _ = () + let latex_string _ = () + + let html_char = output_char + let html_string = output_string + + let start_latex_math () = () + let stop_latex_math () = () + + let start_verbatim () = printf "
"
+  let stop_verbatim () = printf "
\n" + + let module_ref m s = + printf "" m; raw_ident s; printf "" + (*i + match find_module m with + | Local -> + printf "" m; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s + i*) + + let ident_ref m s = match find_module m with + | Local -> + printf "" m s; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m s; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s + + let ident s loc = + if is_keyword s then begin + printf ""; + raw_ident s; + printf "" + end else + try + (match Index.find !current_module loc with + | Def _ -> + printf "" s; raw_ident s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,s') when s = s' -> + ident_ref m s + | Mod _ | Ref _ -> + raw_ident s) + with Not_found -> + raw_ident s + + let with_html_printing f tok = + try + (match Hashtbl.find token_pp tok with + | _, Some s -> output_string s + | _ -> f tok) + with Not_found -> + f tok + + let ident s l = with_html_printing (fun s -> ident s l) s + + let symbol = with_html_printing raw_ident + + let rec reach_item_level n = + if !item_level < n then begin + printf "\n
    \n
  • "; incr item_level; + reach_item_level n + end else if !item_level > n then begin + printf "\n
    • \n
\n"; decr item_level; + reach_item_level n + end + + let item n = + let old_level = !item_level in + reach_item_level n; + if n <= old_level then printf "\n\n
  • " + + let stop_item () = reach_item_level 0 + + let start_coq () = if not !raw_comments then printf "\n" + + let end_coq () = if not !raw_comments then printf "\n" + + let start_doc () = + if not !raw_comments then + printf "\n
    \n" + + let end_doc () = + stop_item (); + if not !raw_comments then printf "\n
    \n" + + let start_code () = end_doc (); start_coq () + + let end_code () = end_coq (); start_doc () + + let start_inline_coq () = printf "" + + let end_inline_coq () = printf "" + + let paragraph () = stop_item (); printf "\n

    \n" + + let section lev f = + let lab = new_label () in + let r = sprintf "%s.html#%s" !current_module lab in + add_toc_entry (Toc_section (lev, f, r)); + stop_item (); + printf "" lab lev; + f (); + printf "\n" lev + + let rule () = printf "
    \n" + + let entry_type = function + | Library -> "library" + | Module -> "module" + | Definition -> "definition" + | Inductive -> "inductive" + | Constructor -> "constructor" + | Lemma -> "lemma" + | Variable -> "variable" + | Axiom -> "axiom" + | TacticDefinition -> "tactic definition" + + (* make a HTML index from a list of triples (name,text,link) *) + let index_ref i c = + let idxc = sprintf "%s_%c" i.idx_name c in + if !multi_index then "index_" ^ idxc ^ ".html" else "index.html#" ^ idxc + + let letter_index category idx (c,l) = + if l <> [] then begin + let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in + printf "

    %c %s

    \n" idx c c cat; + List.iter + (fun (id,(text,link)) -> + printf "%s %s
    \n" link id text) l; + printf "

    " + end + + 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 "
    "; + letter_index true idx cl; + if List.length l > 30 then begin printf "
    "; navig () end; + trailer (); + close () + in + List.iter one_letter i.idx_entries + + let format_global_index = + Index.map + (fun s (m,t) -> + if t = Library then + "[library]", m ^ ".html" + else + sprintf "[%s, in %s]" (entry_type t) m m , + sprintf "%s.html#%s" m s) + + let format_bytype_index = function + | Library, idx -> + Index.map (fun id m -> "", m ^ ".html") idx + | (t,idx) -> + Index.map + (fun s m -> + let text = sprintf "[in %s]" m m in + (text, sprintf "%s.html#%s" m s)) idx + + let navig_one_index i = + printf "\n%s Index\n" (String.capitalize i.idx_name); + List.iter + (fun (c,l) -> + if l <> [] then + printf "%c\n" (index_ref i c) c + else + printf "%c\n" c) + i.idx_entries; + let n = i.idx_size in + printf "(%d %s)\n" n (if n > 1 then "entries" else "entry"); + printf "\n" + + let navig_index il = + printf "\n"; + List.iter navig_one_index il; + printf "
    \n" + + 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"; + current_module := "Index"; + page_title := (if !title <> "" then !title else "Index"); + header (); + if !title <> "" then printf "

    %s

    \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 "
    \n

    %s Index

    \n" (String.capitalize i.idx_name); + all_letters i + end + in + List.iter one_index idxl; + printf "
    "; + navig (); + trailer (); + close () + end; + end + + let make_toc () = + set_out_file "toc.html"; + page_title := (if !title <> "" then !title else "Table of contents"); + header (); + if !title <> "" then printf "

    %s

    \n" !title; + let make_toc_entry = function + | Toc_library m -> + stop_item (); + printf "

    Library %s

    \n" m m + | Toc_section (n, f, r) -> + item n; + printf "" r; f (); printf "\n" + in + Queue.iter make_toc_entry toc_q; + stop_item (); + if !index then printf "

    Index

    "; + trailer (); + close () + +end + + +(*s TeXmacs-aware output *) + +module TeXmacs = struct + + (*s Latex preamble *) + + let in_doc = ref false + + let (preamble : string Queue.t) = + in_doc := false; Queue.create () + + let push_in_preamble s = Queue.add s preamble + + let header () = + output_string + "(*i This file has been automatically generated with the command \n"; + output_string + " "; Array.iter (fun s -> printf "%s " s) Sys.argv; printf " *)\n" + + let trailer () = () + + let char_true c = match c with + | '\\' -> printf "\\\\" + | '<' -> printf "\\<" + | '|' -> printf "\\|" + | '>' -> printf "\\>" + | _ -> output_char c + + let char c = if !in_doc then char_true c else output_char c + + let latex_char = char_true + let latex_string = String.iter latex_char + + let html_char _ = () + let html_string _ = () + + let raw_ident s = + for i = 0 to String.length s - 1 do char s.[i] done + + let start_module () = () + + let start_latex_math () = printf "' + + let start_verbatim () = in_doc := true; printf "<\\verbatim>" + + let stop_verbatim () = in_doc := false; printf "" + + let indentation n = () + + let ident_true s = + if is_keyword s then begin + printf "" + end else begin + raw_ident s + end + + let ident s _ = if !in_doc then ident_true s else raw_ident s + + let symbol_true s = + let ensuremath x = printf ">" x in + match s with + | "*" -> ensuremath "times" + | "->" -> ensuremath "rightarrow" + | "<-" -> ensuremath "leftarrow" + | "<->" ->ensuremath "leftrightarrow" + | "=>" -> ensuremath "Rightarrow" + | "<=" -> ensuremath "le" + | ">=" -> ensuremath "ge" + | "<>" -> ensuremath "noteq" + | "~" -> ensuremath "lnot" + | "/\\" -> ensuremath "land" + | "\\/" -> ensuremath "lor" + | "|-" -> ensuremath "vdash" + | s -> raw_ident s + + let symbol s = if !in_doc then symbol_true s else raw_ident s + + let rec reach_item_level n = + if !item_level < n then begin + printf "\n<\\itemize>\n"; incr item_level; + reach_item_level n + end else if !item_level > n then begin + printf "\n"; decr item_level; + reach_item_level n + end + + let item n = + let old_level = !item_level in + reach_item_level n; + if n <= old_level then printf "\n\n" + + let stop_item () = reach_item_level 0 + + let start_doc () = in_doc := true; printf "(** texmacs: " + + let end_doc () = stop_item (); in_doc := false; printf " *)" + + let start_coq () = () + + let end_coq () = () + + let start_code () = in_doc := true; printf "<\\code>\n" + let end_code () = in_doc := false; printf "\n" + + let section_kind = function + | 1 -> "section" + | 2 -> "subsection" + | 3 -> "subsubsection" + | 4 -> "paragraph" + | _ -> assert false + + let section lev f = + stop_item (); + printf "<"; output_string (section_kind lev); printf "|"; + f (); printf ">\n\n" + + let rule () = + printf "\n\n" + + let paragraph () = stop_item (); printf "\n\n" + + let line_break_true () = printf "" + + let line_break () = printf "\n" + + let empty_line_of_code () = printf "\n" + + let start_inline_coq () = printf "" + + let make_index () = () + + let make_toc () = () + +end + +(*s Generic output *) + +let select f1 f2 f3 x = + match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x + +let push_in_preamble = Latex.push_in_preamble + +let header = select Latex.header Html.header TeXmacs.header +let trailer = select Latex.trailer Html.trailer TeXmacs.trailer + +let start_module = + select Latex.start_module Html.start_module TeXmacs.start_module + +let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc +let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc + +let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq +let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq + +let start_code = select Latex.start_code Html.start_code TeXmacs.start_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code + +let start_inline_coq = + select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq +let end_inline_coq = + select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq + +let indentation = select Latex.indentation Html.indentation TeXmacs.indentation +let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph +let line_break = select Latex.line_break Html.line_break TeXmacs.line_break +let empty_line_of_code = select + Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code + +let section = select Latex.section Html.section TeXmacs.section +let item = select Latex.item Html.item TeXmacs.item +let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item +let rule = select Latex.rule Html.rule TeXmacs.rule + +let char = select Latex.char Html.char TeXmacs.char +let ident = select Latex.ident Html.ident TeXmacs.ident +let symbol = select Latex.symbol Html.symbol TeXmacs.symbol + +let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char +let latex_string = + select Latex.latex_string Html.latex_string TeXmacs.latex_string +let html_char = select Latex.html_char Html.html_char TeXmacs.html_char +let html_string = + select Latex.html_string Html.html_string TeXmacs.html_string + +let start_latex_math = + select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math +let stop_latex_math = + select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math + +let start_verbatim = + select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim +let stop_verbatim = + select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim +let verbatim_char = + select output_char Html.char TeXmacs.char +let hard_verbatim_char = output_char + +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 new file mode 100644 index 00000000..2195fa53 --- /dev/null +++ b/tools/coqdoc/output.mli @@ -0,0 +1,92 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit +val output_dir : string ref +val close : unit -> unit + +val quiet : bool ref +val short : bool ref +val light : bool ref +val header_trailer : bool ref +val index : bool ref +val multi_index : bool ref +val toc : bool ref +val title : string ref +val externals : bool ref +val coqlib : string ref +val raw_comments : bool ref + +val charset : string ref +val inputenc : string ref +val set_latin1 : unit -> unit +val set_utf8 : unit -> unit + +val add_printing_token : string -> string option * string option -> unit +val remove_printing_token : string -> unit + +val set_module : coq_module -> unit + +val header : unit -> unit +val trailer : unit -> unit + +val push_in_preamble : string -> unit + +val dump_file : string -> unit + +val start_module : unit -> unit + +val start_doc : unit -> unit +val end_doc : unit -> unit + +val start_coq : unit -> unit +val end_coq : unit -> unit + +val start_code : unit -> unit +val end_code : unit -> unit + +val start_inline_coq : unit -> unit +val end_inline_coq : unit -> unit + +val indentation : int -> unit +val line_break : unit -> unit +val paragraph : unit -> unit +val empty_line_of_code : unit -> unit + +val section : int -> (unit -> unit) -> unit + +val item : int -> unit + +val rule : unit -> unit + +val char : char -> unit +val ident : string -> loc -> unit +val symbol : string -> unit + +val latex_char : char -> unit +val latex_string : string -> unit +val html_char : char -> unit +val html_string : string -> unit +val verbatim_char : char -> unit +val hard_verbatim_char : char -> unit + +val start_latex_math : unit -> unit +val stop_latex_math : unit -> unit +val start_verbatim : unit -> unit +val stop_verbatim : unit -> unit + +val make_index : unit -> unit +val make_toc : unit -> unit diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli new file mode 100644 index 00000000..07808fe9 --- /dev/null +++ b/tools/coqdoc/pretty.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll new file mode 100644 index 00000000..541939b5 --- /dev/null +++ b/tools/coqdoc/pretty.mll @@ -0,0 +1,586 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* count (c + (8 - (c mod 8))) (i + 1) + | ' ' -> count (c + 1) (i + 1) + | _ -> c + in + count 0 0 + + let count_dashes s = + let c = ref 0 in + for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done; + !c + + let cut_head_tail_spaces s = + let n = String.length s in + let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in + let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in + let l = look_up 0 in + let r = look_dn (n-1) in + if l <= r then String.sub s l (r-l+1) else s + + let sec_title s = + let rec count lev i = + if s.[i] = '*' then + count (succ lev) (succ i) + else + let t = String.sub s i (String.length s - i) in + lev, cut_head_tail_spaces t + in + count 0 (String.index s '*') + + let formatted = ref false + let brackets = ref 0 + + let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + + (* Gallina (skipping proofs). This is a three states automaton. *) + + let gallina = ref false + + type gallina_state = Nothing | AfterDot | Proof + + let gstate = ref AfterDot + + let is_proof = + let t = Hashtbl.create 13 in + List.iter (fun s -> Hashtbl.add t s true) + [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let"; + "Correctness"; "Definition"; "Morphism" ]; + fun s -> try Hashtbl.find t s with Not_found -> false + + let gallina_id id = + if !gstate = AfterDot then + if is_proof id then gstate := Proof else + if id <> "Add" then gstate := Nothing + + let gallina_symbol s = + if !gstate = AfterDot || (!gstate = Proof && s = ":=") then + gstate := Nothing + + let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false + + let gallina_char c = + if c = '.' then + (let skip = !gstate = Proof in gstate := AfterDot; skip) + else + (if !gstate = AfterDot && not (is_space c) then gstate := Nothing; + false) + + (* saving/restoring the PP state *) + + type state = { + st_gallina : bool; + st_light : bool + } + + let state_stack = Stack.create () + + let save_state () = + Stack.push { st_gallina = !gallina; st_light = !light } state_stack + + let restore_state () = + let s = Stack.pop state_stack in + gallina := s.st_gallina; + light := s.st_light + + let without_ref r f x = save_state (); r := false; f x; restore_state () + + let without_gallina = without_ref gallina + + let without_light = without_ref light + + let show_all f = without_gallina (without_light f) + + let begin_show () = save_state (); gallina := false; light := false + let end_show () = restore_state () + + (* Reset the globals *) + + let reset () = + formatted := false; + brackets := 0; + gstate := AfterDot + + (* erasing of Section/End *) + + let section_re = Str.regexp "[ \t]*Section" + let end_re = Str.regexp "[ \t]*End" + let is_section s = Str.string_match section_re s 0 + let is_end s = Str.string_match end_re s 0 + + let sections_to_close = ref 0 + + let section_or_end s = + if is_section s then begin + incr sections_to_close; true + end else if is_end s then begin + if !sections_to_close > 0 then begin + decr sections_to_close; true + end else + false + end else + true + + (* tokens pretty-print *) + + let token_buffer = Buffer.create 1024 + + let token_re = + Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)" + let printing_token_re = + Str.regexp + "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?" + + let add_printing_token toks pps = + try + if Str.string_match token_re toks 0 then + let tok = Str.matched_group 1 toks in + if Str.string_match printing_token_re pps 0 then + let pp = + (try Some (Str.matched_group 3 pps) with _ -> + try Some (Str.matched_group 4 pps) with _ -> None), + (try Some (Str.matched_group 6 pps) with _ -> None) + in + Output.add_printing_token tok pp + with _ -> + () + + let remove_token_re = + Str.regexp + "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)" + + let remove_printing_token toks = + try + if Str.string_match remove_token_re toks 0 then + let tok = Str.matched_group 1 toks in + Output.remove_printing_token tok + with _ -> + () + + let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:=" + let extract_ident s = + assert (String.length s >= 3); + if Str.string_match extract_ident_re s 0 then + Str.matched_group 1 s + else + String.sub s 1 (String.length s - 3) + +} + +(*s Regular expressions *) + +let space = [' ' '\t'] +let space_nl = [' ' '\t' '\n' '\r'] + +let firstchar = + ['A'-'Z' 'a'-'z' '_' + (* iso 8859-1 accents *) + '\192'-'\214' '\216'-'\246' '\248'-'\255' ] | + (* utf-8 latin 1 supplement *) + '\195' ['\128'-'\191'] | + (* utf-8 letterlike symbols *) + '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) +let identchar = + firstchar | ['\'' '0'-'9' '@'] +let identifier = firstchar identchar* + +let symbolchar_no_brackets = + ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' + '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' + '{' '}' '(' ')'] | + (* utf-8 symbols *) + '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ +let symbolchar = symbolchar_no_brackets | '[' | ']' +let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' + +(* tokens with balanced brackets *) +let token_brackets = + ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* + | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ ) + symbolchar_no_brackets* + +let section = "*" | "**" | "***" | "****" + +let item_space = " " + +let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* '\n' +let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* '\n' +let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* '\n' +let end_show = "(*" space* "end" space+ "show" space* "*)" space* '\n' +(* +let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" +let end_verb = "(*" space* "end" space+ "verb" space* "*)" +*) + +let coq_command_to_hide = + "Implicit" space | + "Ltac" space | + "Require" space | + "Load" space | + "Hint" space | + "Transparent" space | + "Opaque" space | + ("Declare" space+ ("Morphism" | "Step") space) | + "Section" space | + "Variable" 's'? space | + ("Hypothesis" | "Hypotheses") space | + "End" space | + ("Set" | "Unset") space+ "Printing" space+ "Coercions" space | + "Declare" space+ ("Left" | "Right") space+ "Step" space + +(*s Scanning Coq, at beginning of line *) + +rule coq_bol = parse + | '\n'+ + { empty_line_of_code (); coq_bol lexbuf } + | space* "(**" space_nl + { end_coq (); start_doc (); + let eol = doc_bol lexbuf in + end_doc (); start_coq (); + if eol then coq_bol lexbuf else coq lexbuf } + | space* "Comments" space_nl + { end_coq (); start_doc (); comments lexbuf; end_doc (); + start_coq (); coq lexbuf } + | space* begin_hide + { skip_hide lexbuf; coq_bol lexbuf } + | space* begin_show + { begin_show (); coq_bol lexbuf } + | space* end_show + { end_show (); coq_bol lexbuf } + | space* coq_command_to_hide + { let s = lexeme lexbuf in + if !light && section_or_end s then begin + skip_to_dot lexbuf; + coq_bol lexbuf + end else begin + indentation (count_spaces s); + backtrack lexbuf; + coq lexbuf + end } + | space* "(**" space+ "printing" space+ (identifier | token) space+ + { let tok = lexeme lexbuf in + let s = printing_token lexbuf in + add_printing_token tok s; + coq_bol lexbuf } + | space* "(**" space+ "printing" space+ + { eprintf "warning: bad 'printing' command at character %d\n" + (lexeme_start lexbuf); flush stderr; + ignore (comment lexbuf); + coq_bol lexbuf } + | space* "(**" space+ "remove" space+ "printing" space+ + (identifier | token) space* "*)" + { remove_printing_token (lexeme lexbuf); + coq_bol lexbuf } + | space* "(**" space+ "remove" space+ "printing" space+ + { eprintf "warning: bad 'remove printing' command at character %d\n" + (lexeme_start lexbuf); flush stderr; + ignore (comment lexbuf); + coq_bol lexbuf } + | space* "(*" + { let eol = comment lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | space+ + { indentation (count_spaces (lexeme lexbuf)); coq lexbuf } + | eof + { () } + | _ + { backtrack lexbuf; indentation 0; coq lexbuf } + +(*s Scanning Coq elsewhere *) + +and coq = parse + | "\n" + { line_break (); coq_bol lexbuf } + | "(**" space_nl + { end_coq (); start_doc (); + let eol = doc_bol lexbuf in + end_doc (); start_coq (); + if eol then coq_bol lexbuf else coq lexbuf } + | "(*" + { let eol = comment lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | '\n'+ space* "]]" + { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end } + | eof + { () } + | token + { let s = lexeme lexbuf in + if !gallina then gallina_symbol s; + symbol s; + coq lexbuf } + | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module" + (* hack to avoid making Type a keyword *) + { let s = lexeme lexbuf in + if !gallina then gallina_id s; + ident s (lexeme_start lexbuf); coq lexbuf } + | "(" space* identifier space* ":=" + { let id = extract_ident (lexeme lexbuf) in + symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf } + | (identifier '.')* identifier + { let id = lexeme lexbuf in + if !gallina then gallina_id id; + ident id (lexeme_start lexbuf); coq lexbuf } + | _ + { let c = lexeme_char lexbuf 0 in + char c; + if !gallina && gallina_char c then skip_proof lexbuf; + coq lexbuf } + +(*s Scanning documentation, at beginning of line *) + +and doc_bol = parse + | space* "\n" '\n'* + { paragraph (); doc_bol lexbuf } + | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])* + { let lev, s = sec_title (lexeme lexbuf) in + section lev (fun () -> ignore (doc (from_string s))); + doc lexbuf } + | space* '-'+ + { let n = count_dashes (lexeme lexbuf) in + if n >= 4 then rule () else item n; + doc lexbuf } + | "<<" space* + { start_verbatim (); verbatim lexbuf; doc_bol lexbuf } + | eof + { false } + | _ + { backtrack lexbuf; doc lexbuf } + +(*s Scanning documentation elsewhere *) + +and doc = parse + | "\n" + { char '\n'; doc_bol lexbuf } + | "[" + { brackets := 1; + start_inline_coq (); escaped_coq lexbuf; end_inline_coq (); + doc lexbuf } + | "[[" '\n' space* + { formatted := true; start_code (); + indentation (count_spaces (lexeme lexbuf)); + without_gallina coq lexbuf; + end_code (); formatted := false; + doc lexbuf } + | '*'* "*)" space* '\n' + { true } + | '*'* "*)" + { false } + | "$" + { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf } + | "$$" + { char '$'; doc lexbuf } + | "%" + { escaped_latex lexbuf; doc lexbuf } + | "%%" + { char '%'; doc lexbuf } + | "#" + { escaped_html lexbuf; doc lexbuf } + | "##" + { char '#'; doc lexbuf } + | eof + { false } + | _ + { char (lexeme_char lexbuf 0); doc lexbuf } + +(*s Various escapings *) + +and escaped_math_latex = parse + | "$" { stop_latex_math () } + | eof { stop_latex_math () } + | _ { latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf } + +and escaped_latex = parse + | "%" { () } + | eof { () } + | _ { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } + +and escaped_html = parse + | "#" { () } + | "&#" + { html_char '&'; html_char '#'; escaped_html lexbuf } + | "##" + { html_char '#'; escaped_html lexbuf } + | eof { () } + | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf } + +and verbatim = parse + | "\n>>" { verbatim_char '\n'; stop_verbatim () } + | eof { stop_verbatim () } + | _ { verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf } + +(*s Coq, inside quotations *) + +and escaped_coq = parse + | "]" + { decr brackets; + if !brackets > 0 then begin char ']'; escaped_coq lexbuf end } + | "[" + { incr brackets; char '['; escaped_coq lexbuf } + | "(*" + { ignore (comment lexbuf); escaped_coq lexbuf } + | "*)" + { (* likely to be a syntax error: we escape *) backtrack lexbuf } + | eof + { () } + | token_brackets + { let s = lexeme lexbuf in + symbol s; + escaped_coq lexbuf } + | (identifier '.')* identifier + { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } + | _ + { char (lexeme_char lexbuf 0); escaped_coq lexbuf } + +(*s Coq "Comments" command. *) + +and comments = parse + | space_nl+ + { char ' '; comments lexbuf } + | '"' [^ '"']* '"' + { let s = lexeme lexbuf in + let s = String.sub s 1 (String.length s - 2) in + ignore (doc (from_string s)); comments lexbuf } + | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+ + { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf } + | "." (space_nl | eof) + { () } + | eof + { () } + | _ + { char (lexeme_char lexbuf 0); comments lexbuf } + +(*s Skip comments *) + +and comment = parse + | "(*" { ignore (comment lexbuf); comment lexbuf } + | "*)" space* '\n'+ { true } + | "*)" { false } + | eof { false } + | _ { comment lexbuf } + +(*s Skip proofs *) + +and skip_proof = parse + | "(*" { ignore (comment lexbuf); skip_proof lexbuf } + | "Save" | "Qed" | "Defined" + | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf } + | "Proof" space* '.' { skip_proof lexbuf } + | identifier { skip_proof lexbuf } (* to avoid keywords within idents *) + | eof { () } + | _ { skip_proof lexbuf } + +and skip_to_dot = parse + | eof | '.' { if !gallina then gstate := AfterDot } + | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf } + | _ { skip_to_dot lexbuf } + +and skip_hide = parse + | eof | end_hide { () } + | _ { skip_hide lexbuf } + +(*s Reading token pretty-print *) + +and printing_token = parse + | "*)" | eof + { let s = Buffer.contents token_buffer in + Buffer.clear token_buffer; + s } + | _ { Buffer.add_string token_buffer (lexeme lexbuf); + printing_token lexbuf } + +(*s Applying the scanners to files *) + +{ + + type file = + | Vernac_file of string * coq_module + | Latex_file of string + + let coq_file f m = + reset (); + Index.scan_file f m; + start_module (); + let c = open_in f in + let lb = from_channel c in + start_coq (); coq_bol lb; end_coq (); + close_in c + + (* LaTeX document *) + + let latex_document l = + let file = function + | Vernac_file (f,m) -> set_module m; coq_file f m + | Latex_file f -> dump_file f + in + header (); + if !toc then make_toc (); + List.iter file l; + trailer (); + close () + + (* HTML document *) + + let html_document l = + let file = function + | Vernac_file (f,m) -> + set_module m; + let hf = m ^ ".html" in + set_out_file hf; + header (); + coq_file f m; + trailer (); + close () + | Latex_file _ -> () + in + List.iter file l; + make_index (); + if !toc then make_toc () + + (* TeXmacs document *) + + let texmacs_document l = + let file = function + | Vernac_file (f,m) -> set_module m; coq_file f m + | Latex_file f -> dump_file f + in + header (); + List.iter file l; + trailer (); + close () + + let index_module = function + | Vernac_file (_,m) -> Index.add_module m + | Latex_file _ -> () + + let produce_document l = + List.iter index_module l; + (match !target_language with + | LaTeX -> latex_document + | HTML -> html_document + | TeXmacs -> texmacs_document) l + +} + diff --git a/tools/coqdoc/style.css b/tools/coqdoc/style.css new file mode 100644 index 00000000..5150bd75 --- /dev/null +++ b/tools/coqdoc/style.css @@ -0,0 +1,23 @@ +a:visited {color : #416DFF; text-decoration : none; } +a:link {color : #416DFF; text-decoration : none; font-weight : bold} +a:hover {color : Red; text-decoration : underline; } +a:active {color : Red; text-decoration : underline; } +.keyword { font-weight : bold ; color : Red } +.keywordsign { color : #C04600 } +.superscript { font-size : 4 } +.subscript { font-size : 4 } +.comment { color : Green } +.constructor { color : Blue } +.string { color : Maroon } +.warning { color : Red ; font-weight : bold } +.info { margin-left : 3em; margin-right : 3em } +.title1 { font-size : 20pt ; background-color : #416DFF } +.title2 { font-size : 20pt ; background-color : #418DFF } +.title3 { font-size : 20pt ; background-color : #41ADFF } +.title4 { font-size : 20pt ; background-color : #41CDFF } +.title5 { font-size : 20pt ; background-color : #41EDFF } +.title6 { font-size : 20pt ; background-color : #41FFFF } +body { background-color : White } +tr { background-color : White } +# .doc { background-color :#aaeeff } +.doc { background-color :#66ff66 } -- cgit v1.2.3