From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- tools/coqdoc/cdglobals.ml | 8 +- tools/coqdoc/coqdoc.sty | 126 +++++++++++++-- tools/coqdoc/index.mli | 18 ++- tools/coqdoc/index.mll | 145 ++++++++++++----- tools/coqdoc/main.ml | 391 ++++++++++++++++++++++++---------------------- tools/coqdoc/output.ml | 193 ++++++++++++++++------- tools/coqdoc/pretty.mll | 319 +++++++++++++++++++++---------------- 7 files changed, 764 insertions(+), 436 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 8a774876..44b9bd3c 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -26,14 +26,18 @@ let out_to = ref MultFiles let out_channel = ref stdout let open_out_file f = - let f = if !output_dir <> "" then Filename.concat !output_dir f else f in + let f = if !output_dir <> "" && Filename.is_relative f then Filename.concat !output_dir f else f in out_channel := open_out f let close_out_file () = close_out !out_channel let header_trailer = ref true -let quiet = ref false +let header_file = ref "" +let header_file_spec = ref false +let footer_file = ref "" +let footer_file_spec = ref false +let quiet = ref true let light = ref false let gallina = ref false let short = ref false diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 2c07b9fc..d31314c5 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -8,20 +8,20 @@ \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{coqdoc}[2002/02/11] -% Headings -\usepackage{fancyhdr} -\newcommand{\coqdocleftpageheader}{\thepage\ -- \today} -\newcommand{\coqdocrightpageheader}{\today\ -- \thepage} -\pagestyle{fancyplain} +% % Headings +% \usepackage{fancyhdr} +% \newcommand{\coqdocleftpageheader}{\thepage\ -- \today} +% \newcommand{\coqdocrightpageheader}{\today\ -- \thepage} +% \pagestyle{fancyplain} -%BEGIN LATEX -\headsep 8mm -\renewcommand{\plainheadrulewidth}{0.4pt} -\renewcommand{\plainfootrulewidth}{0pt} -\lhead[\coqdocleftpageheader]{\leftmark} -\rhead[\leftmark]{\coqdocrightpageheader} -\cfoot{} -%END LATEX +% %BEGIN LATEX +% \headsep 8mm +% \renewcommand{\plainheadrulewidth}{0.4pt} +% \renewcommand{\plainfootrulewidth}{0pt} +% \lhead[\coqdocleftpageheader]{\leftmark} +% \rhead[\leftmark]{\coqdocrightpageheader} +% \cfoot{} +% %END LATEX % Hevea puts to much space with \medskip and \bigskip %HEVEA\renewcommand{\medskip}{} @@ -36,11 +36,27 @@ %END LATEX % macro for typesetting keywords -\newcommand{\coqdockw}[1]{\textsf{#1}} +\newcommand{\coqdockw}[1]{\texttt{#1}} -% macro for typesetting identifiers +% macro for typesetting variable identifiers \newcommand{\coqdocid}[1]{\textit{#1}} +% macro for typesetting constant identifiers +\newcommand{\coqdoccst}[1]{\textsf{#1}} + +% macro for typesetting module identifiers +\newcommand{\coqdocmod}[1]{\textsc{\textsf{#1}}} + +% macro for typesetting module constant identifiers (e.g. Parameters in +% module types) +\newcommand{\coqdocax}[1]{\textsl{\textsf{#1}}} + +% macro for typesetting inductive type identifiers +\newcommand{\coqdocind}[1]{\textbf{\textsf{#1}}} + +% macro for typesetting constructor identifiers +\newcommand{\coqdocconstr}[1]{\textsf{#1}} + % newline and indentation %BEGIN LATEX \newcommand{\coqdoceol}{\setlength\parskip{0pt}\par} @@ -52,6 +68,86 @@ % macro for typesetting the title of a module implementation \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } +\usepackage{ifpdf} +\ifpdf + \usepackage[pdftex]{hyperref} + \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black} + \usepackage[all]{hypcap} + + \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}} + \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}} + \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}} + \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection + \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}} +\else + \newcommand{\coqdef}[3]{#3} + \newcommand{\coqref}[2]{#2} + \newcommand{\identref}[2]{\textsf {#2}} + \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}} +\fi +\usepackage{xr} + +%\usepackage{color} +%\usepackage{multind} +%\newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}} + + + +\newcommand{\coqdocvar}[1]{{\textit{#1}}} +\newcommand{\coqdoctac}[1]{{\texttt{#1}}} + + +\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +%\newcommand{\coqvariable}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} +%\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocid{#2}}} +\newcommand{\coqvariable}[2]{\coqdocid{#2}} + +\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}} +\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}} + +\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} +\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}} + +\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}} + +\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}} + +%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}} + +\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}} + +\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}} +\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}} + +\newcommand{\coqmodule}[2]{\coqdef{#1}{#2}{\coqdocmod{#2}}} +\newcommand{\coqmoduleref}[2]{\coqref{#1}{\coqdocmod{#2}}} + %HEVEA\newcommand{\lnot}{\coqwkw{not}} %HEVEA\newcommand{\lor}{\coqwkw{or}} diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 4b53d6ff..1da8ebd7 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mli 8617 2006-03-08 10:47:12Z notin $ i*) +(*i $Id: index.mli 11065 2008-06-06 22:39:43Z msozeau $ i*) open Cdglobals @@ -19,13 +19,23 @@ type entry_type = | Inductive | Constructor | Lemma + | Record + | Projection + | Instance + | Class + | Method | Variable | Axiom | TacticDefinition + | Abbreviation + | Notation + | Section + +val type_name : entry_type -> string type index_entry = | Def of string * entry_type - | Ref of coq_module * string + | Ref of coq_module * string * entry_type | Mod of coq_module * string val find : coq_module -> loc -> index_entry @@ -42,7 +52,7 @@ val scan_file : string -> coq_module -> unit (*s Read globalizations from a file (produced by coqc -dump-glob) *) -val read_glob : string -> unit +val read_glob : string -> coq_module (*s Indexes *) @@ -51,6 +61,8 @@ type 'a index = { idx_entries : (char * (string * 'a) list) list; idx_size : int } +val current_library : string ref + val all_entries : unit -> (coq_module * entry_type) index * (entry_type * coq_module index) list diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 5b281b8b..fc2090dc 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* "<>" then + if id <> "<>" then + sp ^ "." ^ id + else sp + else if id <> "<>" + then id + else "" + +let add_def loc ty sp id = + Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty)) +let add_ref m loc m' sp id ty = + Hashtbl.add table (m, loc) (Ref (m', full_ident sp id, ty)) + let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id)) let find m l = Hashtbl.find table (m, l) - (*s Manipulating path prefixes *) type stack = string list @@ -99,14 +118,15 @@ let make_fullid id = else id + (* Coq modules *) let split_sp s = try let i = String.rindex s '.' in - String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1) - with Not_found -> - "", s + String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1) + with + Not_found -> "", s let modules = Hashtbl.create 97 let local_modules = Hashtbl.create 97 @@ -118,8 +138,7 @@ let add_module m = type module_kind = Local | Coqlib | Unknown -let coq_module m = - String.length m >= 4 && String.sub m 0 4 = "Coq." +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 @@ -129,14 +148,6 @@ let find_module m = 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_library (loc+i+1) (Hashtbl.find modules id) id - with Not_found -> - () (* Building indexes *) @@ -181,10 +192,18 @@ let type_name = function | Inductive -> "inductive" | Constructor -> "constructor" | Lemma -> "lemma" + | Record -> "record" + | Projection -> "projection" + | Instance -> "instance" + | Class -> "class" + | Method -> "method" | Variable -> "variable" | Axiom -> "axiom" | TacticDefinition -> "tactic" - + | Abbreviation -> "abbreviation" + | Notation -> "notation" + | Section -> "section" + let all_entries () = let gl = ref [] in let add_g s m t = gl := (s,(m,t)) :: !gl in @@ -209,6 +228,8 @@ let all_entries () = } (*s Shortcuts for regular expressions. *) +let digit = ['0'-'9'] +let num = digit+ let space = [' ' '\010' '\013' '\009' '\012'] @@ -225,16 +246,18 @@ let end_hide = "(*" space* "end" space+ "hide" space* "*)" (*s Indexing entry point. *) rule traverse = parse - | "Definition" space + | ("Program" space+)? "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 + | ("Program" space+)? "Fixpoint" space { current_type := Definition; index_ident lexbuf; fixpoint lexbuf; traverse lexbuf } - | ("Lemma" | "Theorem") space + | ("Program" space+)? ("Lemma" | "Theorem") space + { current_type := Lemma; index_ident lexbuf; traverse lexbuf } + | "Obligation" space num ("of" ident)? { current_type := Lemma; index_ident lexbuf; traverse lexbuf } | "Inductive" space { current_type := Inductive; @@ -247,8 +270,8 @@ rule traverse = parse | "Variable" 's'? space { current_type := Variable; index_idents lexbuf; traverse lexbuf } ***i*) - | "Require" (space+ ("Export"|"Import"))? space+ ident - { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf } + | "Require" (space+ ("Export"|"Import"))? + { module_refs lexbuf; traverse lexbuf } | "End" space+ { end_ident lexbuf; traverse lexbuf } | begin_hide @@ -277,7 +300,7 @@ and index_ident = parse | Lemma -> make_fullid id | _ -> id in - add_def (lexeme_start lexbuf) !current_type fullid } + add_def (lexeme_start lexbuf) !current_type "" fullid } | eof { () } | _ @@ -289,7 +312,7 @@ and index_idents = parse | space+ | ',' { index_idents lexbuf } | ident - { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf); + { add_def (lexeme_start lexbuf) !current_type "" (lexeme lexbuf); index_idents lexbuf } | eof { () } @@ -369,14 +392,52 @@ and module_ident = parse { () } | ident { let id = lexeme lexbuf in - begin_module id; add_def (lexeme_start lexbuf) !current_type id } + begin_module id; add_def (lexeme_start lexbuf) !current_type "" id } | eof { () } | _ { () } +(*s parse module names *) + +and module_refs = parse + | space+ + { module_refs lexbuf } + | ident + { let id = lexeme lexbuf in + (try + add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id + with + Not_found -> () + ); + module_refs lexbuf } + | eof + { () } + | _ + { () } + { - + let type_of_string = function + | "def" | "coe" | "subclass" | "canonstruc" + | "ex" | "scheme" -> Definition + | "prf" | "thm" -> Lemma + | "ind" | "coind" -> Inductive + | "constr" -> Constructor + | "rec" | "corec" -> Record + | "proj" -> Projection + | "class" -> Class + | "meth" -> Method + | "inst" -> Instance + | "var" -> Variable + | "defax" | "prfax" | "ax" -> Axiom + | "syndef" -> Abbreviation + | "not" -> Notation + | "lib" -> Library + | "mod" | "modtype" -> Module + | "tac" -> TacticDefinition + | "sec" -> Section + | s -> raise (Invalid_argument ("type_of_string:" ^ s)) + let read_glob f = let c = open_in f in let cur_mod = ref "" in @@ -387,22 +448,22 @@ and module_ident = parse if n > 0 then begin match s.[0] with | 'F' -> - cur_mod := String.sub s 1 (n - 1) + cur_mod := String.sub s 1 (n - 1); + current_library := !cur_mod | 'R' -> (try - let i = String.index s ' ' in - let j = String.index_from s (i+1) ' ' in - let loc = int_of_string (String.sub s 1 (i - 1)) in - let lib_dp = String.sub s (i + 1) (j - i - 1) in - let full_id = String.sub s (j + 1) (n - j - 1) in - add_ref !cur_mod loc lib_dp full_id - with Not_found -> - ()) - | _ -> () + Scanf.sscanf s "R%d %s %s %s %s" + (fun loc lib_dp sp id ty -> + add_ref !cur_mod loc lib_dp sp id (type_of_string ty)) + with _ -> ()) + | _ -> + try Scanf.sscanf s "%s %d %s %s" + (fun ty loc sp id -> add_def loc (type_of_string ty) sp id) + with Scanf.Scan_failure _ -> () end - done + done; assert false with End_of_file -> - close_in c + close_in c; !cur_mod let scan_file f m = init_stack (); current_library := m; diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 18a44a44..7111187f 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -19,50 +20,53 @@ *) open Cdglobals -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 " --stdout write output to stdout"; - 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 " --coqlib_path set the path where Coq files are installed"; - 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 " --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 " --pdf output the Pdf"; + prerr_endline " --stdout write output to stdout"; + 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 " --with-header prepend as html reader"; + prerr_endline " --with-footer append as html footer"; + 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 (default)"; + prerr_endline " --verbose verbose mode"; + 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 " --coqlib_path set the path where Coq files are installed"; + 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 ""; exit 1 +let obsolete s = + eprintf "Warning: option %s is now obsolete; please update your scripts\n" s + (*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 @@ -74,7 +78,7 @@ let banner () = flush stderr let target_full_name f = - match !target_language with + match !Cdglobals.target_language with | HTML -> f ^ ".html" | _ -> f ^ ".tex" @@ -88,95 +92,70 @@ let check_if_file_exists f = eprintf "\ncoqdoc: %s: no such file\n" f; exit 1 end - + + +(*s Manipulations of paths and path aliases *) + +let normalize_path p = + (* We use the Unix subsystem to normalize a physical path (relative + or absolute) and get rid of symbolic links, relative links (like + ./ or ../ in the middle of the path; it's tricky but it + works... *) + (* Rq: Sys.getcwd () returns paths without '/' at the end *) + let orig = Sys.getcwd () in + Sys.chdir p; + let res = Sys.getcwd () in + Sys.chdir orig; + res + +let normalize_filename f = + let basename = Filename.basename f in + let dirname = Filename.dirname f in + Filename.concat (normalize_path dirname) basename + +(* [paths] maps a physical path to a name *) let paths = ref [] -let add_path m l = paths := (m,l) :: !paths +let add_path dir name = + (* if dir is relative we add both the relative and absolute name *) + let p = normalize_path dir in + paths := (p,name) :: !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 name_of_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 coq_module filename = + let bfname = Filename.chop_extension filename in + let nfname = normalize_filename bfname in + let rec change_prefix map f = + match map with + | [] -> + (* There is no prefix alias; + we just cut the name wrt current working directory *) + let cwd = Sys.getcwd () in + let exp = Str.regexp (Str.quote (cwd ^ "/")) in + if (Str.string_match exp f 0) then + name_of_path (Str.replace_first exp "" f) + else + name_of_path f + | (p, name) :: rem -> + let expp = Str.regexp (Str.quote p) in + if (Str.string_match expp f 0) then + let newp = Str.replace_first expp name f in + name_of_path newp + else + change_prefix rem f + in + change_prefix !paths nfname let what_file f = check_if_file_exists f; - if check_suffix f ".v" || check_suffix f ".g" then + if Filename.check_suffix f ".v" || Filename.check_suffix f ".g" then Vernac_file (f, coq_module f) - else if check_suffix f ".tex" then + else if Filename.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 + else + (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1) (*s \textbf{Reading file names from a file.} * File names may be given @@ -214,9 +193,9 @@ let files_from_file f = (*s \textbf{Parsing of the command line.} *) -let output_file = ref "" let dvi = ref false let ps = ref false +let pdf = ref false let parse () = let files = ref [] in @@ -227,8 +206,16 @@ let parse () = | ("-nopreamble" | "--nopreamble" | "--no-preamble" | "-bodyonly" | "--bodyonly" | "--body-only") :: rem -> header_trailer := false; parse_rec rem + | ("-with-header" | "--with-header") :: f ::rem -> + header_trailer := true; header_file_spec := true; header_file := f; parse_rec rem + | ("-with-header" | "--with-header") :: [] -> + usage () + | ("-with-footer" | "--with-footer") :: f ::rem -> + header_trailer := true; footer_file_spec := true; footer_file := f; parse_rec rem + | ("-with-footer" | "--with-footer") :: [] -> + usage () | ("-p" | "--preamble") :: s :: rem -> - push_in_preamble s; parse_rec rem + Output.push_in_preamble s; parse_rec rem | ("-p" | "--preamble") :: [] -> usage () | ("-noindex" | "--noindex" | "--no-index") :: rem -> @@ -259,6 +246,8 @@ let parse () = usage () | ("-latex" | "--latex") :: rem -> Cdglobals.target_language := LaTeX; parse_rec rem + | ("-pdf" | "--pdf") :: rem -> + Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem | ("-dvi" | "--dvi") :: rem -> Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem | ("-ps" | "--ps") :: rem -> @@ -284,10 +273,12 @@ let parse () = | ("-q" | "-quiet" | "--quiet") :: rem -> quiet := true; parse_rec rem + | ("-v" | "-verbose" | "--verbose") :: rem -> + quiet := false; parse_rec rem | ("-h" | "-help" | "-?" | "--help") :: rem -> banner (); usage () - | ("-v" | "-version" | "--version") :: _ -> + | ("-V" | "-version" | "--version") :: _ -> banner (); exit 0 | ("-vernac-file" | "--vernac-file") :: f :: rem -> @@ -309,7 +300,7 @@ let parse () = | "-R" :: ([] | [_]) -> usage () | ("-glob-from" | "--glob-from") :: f :: rem -> - Index.read_glob f; parse_rec rem + obsolete "glob-from"; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> @@ -332,7 +323,7 @@ let parse () = (*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. *) + we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *) let locally dir f x = let cwd = Sys.getcwd () in @@ -346,8 +337,10 @@ let clean_temp_files basefile = remove (basefile ^ ".tex"); remove (basefile ^ ".log"); remove (basefile ^ ".aux"); + remove (basefile ^ ".toc"); remove (basefile ^ ".dvi"); remove (basefile ^ ".ps"); + remove (basefile ^ ".pdf"); remove (basefile ^ ".haux"); remove (basefile ^ ".html") @@ -370,70 +363,81 @@ let copy src dst = (*s Functions for generating output files *) - + let gen_one_file l = let file = function | Vernac_file (f,m) -> - set_module m; coq_file f m + Output.set_module m; Pretty.coq_file f m | Latex_file _ -> () in - if (!header_trailer) then header (); - if !toc then make_toc (); + if (!header_trailer) then Output.header (); + if !toc then Output.make_toc (); List.iter file l; - if !index then make_index(); - if (!header_trailer) then trailer () + if !index then Output.make_index(); + if (!header_trailer) then Output.trailer () let gen_mult_files l = let file = function | Vernac_file (f,m) -> - set_module m; + Output.set_module m; let hf = target_full_name m in open_out_file hf; - if (!header_trailer) then header (); - if !toc then make_toc (); - coq_file f m; - if (!header_trailer) then trailer (); + if (!header_trailer) then Output.header (); + Pretty.coq_file f m; + if (!header_trailer) then Output.trailer (); close_out_file() | Latex_file _ -> () in List.iter file l; if (!index && !target_language=HTML) then begin - if (!multi_index) then make_multi_index (); + if (!multi_index) then Output.make_multi_index (); open_out_file "index.html"; page_title := (if !title <> "" then !title else "Index"); - if (!header_trailer) then header (); - make_index (); - if (!header_trailer) then trailer (); + if (!header_trailer) then Output.header (); + Output.make_index (); + if (!header_trailer) then Output.trailer (); close_out_file() end; if (!toc && !target_language=HTML) then begin open_out_file "toc.html"; page_title := (if !title <> "" then !title else "Table of contents"); - if (!header_trailer) then header (); + if (!header_trailer) then Output.header (); if !title <> "" then printf "

%s

\n" !title; - make_toc (); - if (!header_trailer) then trailer (); + Output.make_toc (); + if (!header_trailer) then Output.trailer (); close_out_file() end (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *) +let read_glob x = + match x with + | Vernac_file (f,m) -> + let glob = (Filename.chop_extension f) ^ ".glob" in + (try + Vernac_file (f, Index.read_glob glob) + with _ -> + eprintf "Warning: file %s cannot be opened; links will not be available\n" glob; + x) + | Latex_file _ -> x let index_module = function - | Vernac_file (_,m) -> Index.add_module m + | Vernac_file (f,m) -> + Index.add_module m | Latex_file _ -> () let produce_document l = - List.iter index_module l; (if !target_language=HTML then let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in copy src dst); (if !target_language=LaTeX then - let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in - let dst = if !output_dir <> "" then - Filename.concat !output_dir "coqdoc.sty" - else "coqdoc.sty" in - copy src dst); + let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in + let dst = if !output_dir <> "" then + Filename.concat !output_dir "coqdoc.sty" + else "coqdoc.sty" in + copy src dst); + let l = List.map read_glob l in + List.iter index_module l; match !out_to with | StdOut -> Cdglobals.out_channel := stdout; @@ -446,51 +450,64 @@ let produce_document l = gen_mult_files l let produce_output fl = - if not (!dvi || !ps) then begin + if not (!dvi || !ps || !pdf) then produce_document fl - end else begin - let texfile = temp_file "coqdoc" ".tex" in - let basefile = chop_suffix texfile ".tex" in - open_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 + else + begin + let texfile = Filename.temp_file "coqdoc" ".tex" in + let basefile = Filename.chop_suffix texfile ".tex" in + let final_out_to = !out_to in + out_to := File texfile; + output_dir := (Filename.dirname texfile); + produce_document fl; + + let latexexe = if !pdf then "pdflatex" else "latex" in + let latexcmd = + let file = Filename.basename texfile in + let file = + if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file + in + sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "") 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 + let res = locally (Filename.dirname texfile) Sys.command latexcmd 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 + match final_out_to with + | MultFiles | StdOut -> cat dvifile + | File f -> copy dvifile f end; - if !output_file = "" then cat psfile - end; - clean_temp_files basefile - end + let pdffile = basefile ^ ".pdf" in + if !pdf then + begin + match final_out_to with + | MultFiles | StdOut -> cat pdffile + | File f -> copy pdffile f + end; + if !ps then begin + let psfile = 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; + match final_out_to with + | MultFiles | StdOut -> cat psfile + | File f -> copy psfile f + end; + + clean_temp_files basefile + end (*s \textbf{Main program.} Print the banner, parse the command line, diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d0bc6c2..93414f22 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* Hashtbl.add token_pp s (Some l, None)) [ "*" , "\\ensuremath{\\times}"; + "|", "\\ensuremath{|}"; "->", "\\ensuremath{\\rightarrow}"; "->~", "\\ensuremath{\\rightarrow\\lnot}"; "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}"; @@ -153,6 +171,12 @@ module Latex = struct | _ -> output_char c + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + output_char c + let latex_char = output_char let latex_string = output_string @@ -162,9 +186,14 @@ module Latex = struct let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + let label_ident s = + for i = 0 to String.length s - 1 do label_char s.[i] done + let start_module () = if not !short then begin - printf "\\coqdocmodule{"; + printf "\\coqlibrary{"; + label_ident !current_module; + printf "}{"; raw_ident !current_module; printf "}\n\n" end @@ -192,11 +221,53 @@ module Latex = struct with Not_found -> f tok - let ident s _ = + let module_ref m s = + printf "\\moduleid{%s}{" 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 fid typ s = + let id = if fid <> "" then (m ^ "." ^ fid) else m in + match find_module m with + | Local -> + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" + | Coqlib when !externals -> + let _m = Filename.concat !coqlib m in + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" + | Coqlib | Unknown -> + raw_ident s + + let defref m id ty s = + printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin - printf "\\coqdocid{"; raw_ident s; printf "}" + begin + try + (match Index.find !current_module loc with + | Def (fullid,typ) -> + defref !current_module fullid typ s + | Mod (m,s') when s = s' -> + module_ref m s + | Ref (m,fullid,typ) -> + ident_ref m fullid typ s + | Mod _ -> + printf "\\coqdocid{"; raw_ident s; printf "}") + with Not_found -> + if is_tactic s then begin + printf "\\coqdoctac{"; raw_ident s; printf "}" + end else begin printf "\\coqdocvar{"; raw_ident s; printf "}" end + end end let ident s l = with_latex_printing (fun s -> ident s l) s @@ -271,31 +342,51 @@ end module Html = struct let header () = - if !header_trailer then begin - printf "\n"; - printf "\n\n"; - printf "\n" !charset; - printf "\n"; - printf "%s\n\n\n" !page_title; - printf "\n\n
\n\n
\n
\n\n"; - printf "
\n\n" - end + if !header_trailer then + if !header_file_spec then + let cin = Pervasives.open_in !header_file in + try + while true do + let s = Pervasives.input_line cin in + printf "%s\n" s + done + with End_of_file -> Pervasives.close_in cin + else + begin + printf "\n"; + printf "\n\n"; + printf "\n" !charset; + printf "\n"; + printf "%s\n\n\n" !page_title; + printf "\n\n
\n\n
\n
\n\n"; + printf "
\n\n" + end let self = "http://coq.inria.fr" let trailer () = if !index && !current_module <> "Index" then printf "
\n\n
\n
Index"; - if !header_trailer then begin - printf "
This page has been generated by "; - printf "coqdoc\n" self; - printf "
\n\n
\n\n\n" - end + if !header_trailer then + if !footer_file_spec then + let cin = Pervasives.open_in !footer_file in + try + while true do + let s = Pervasives.input_line cin in + printf "%s\n" s + done + with End_of_file -> Pervasives.close_in cin + else + begin + printf "
This page has been generated by "; + printf "coqdoc\n" self; + printf "
\n\n
\n\n\n" + end let start_module () = if not !short then begin - (* add_toc_entry (Toc_library !current_module); *) + add_toc_entry (Toc_library !current_module); printf "

Library %s

\n\n" !current_module end @@ -338,14 +429,15 @@ module Html = struct raw_ident s i*) - let ident_ref m fid s = match find_module m with - | Local -> - printf "" m fid; raw_ident s; printf "" - | Coqlib when !externals -> - let m = Filename.concat !coqlib m in - printf "" m fid; raw_ident s; printf "" - | Coqlib | Unknown -> - raw_ident s + let ident_ref m fid s = + match find_module m with + | Local -> + printf "" m fid; raw_ident s; printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" m fid; raw_ident s; printf "" + | Coqlib | Unknown -> + raw_ident s let ident s loc = if is_keyword s then begin @@ -360,9 +452,9 @@ module Html = struct printf "" fullid; raw_ident s | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid) -> + | Ref (m,fullid,ty) -> ident_ref m fullid s - | Mod _ | Ref _ -> + | Mod _ -> raw_ident s) with Not_found -> raw_ident s @@ -429,17 +521,6 @@ module Html = struct 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 @@ -465,7 +546,7 @@ module Html = struct if t = Library then "[library]", m ^ ".html" else - sprintf "[%s, in %s]" (entry_type t) m m , + sprintf "[%s, in %s]" (type_name t) m m , sprintf "%s.html#%s" m s) let format_bytype_index = function @@ -548,8 +629,8 @@ module Html = struct item n; printf "" r; f (); printf "\n" in - Queue.iter make_toc_entry toc_q; - stop_item (); + Queue.iter make_toc_entry toc_q; + stop_item (); end diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index e16c7979..8be3e0b0 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* count (c + (8 - (c mod 8))) (i + 1) | ' ' -> count (c + 1) (i + 1) - | _ -> c + | _ -> c,i in - count 0 0 + count 0 0 let count_dashes s = let c = ref 0 in @@ -52,6 +49,11 @@ in count 0 (String.index s '*') + let strip_eol s = + let eol = s.[String.length s - 1] = '\n' in + (eol, if eol then String.sub s 1 (String.length s - 1) else s) + + let formatted = ref false let brackets = ref 0 @@ -69,22 +71,22 @@ let state_stack = Stack.create () let save_state () = - Stack.push { st_gallina = !gallina; st_light = !light } state_stack + Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack let restore_state () = let s = Stack.pop state_stack in - gallina := s.st_gallina; - light := s.st_light + Cdglobals.gallina := s.st_gallina; + Cdglobals.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_gallina = without_ref Cdglobals.gallina - let without_light = without_ref light + let without_light = without_ref Cdglobals.light let show_all f = without_gallina (without_light f) - let begin_show () = save_state (); gallina := false; light := false + let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () (* Reset the globals *) @@ -163,15 +165,20 @@ let space = [' ' '\t'] let space_nl = [' ' '\t' '\n' '\r'] +let nl = "\r\n" | '\n' let firstchar = ['A'-'Z' 'a'-'z' '_' (* iso 8859-1 accents *) '\192'-'\214' '\216'-'\246' '\248'-'\255' ] | + '\194' '\185' | (* utf-8 latin 1 supplement *) '\195' ['\128'-'\191'] | (* utf-8 letterlike symbols *) - '\226' ('\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) + '\206' ['\177'-'\183'] | + '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) + | '\129' [ '\176'-'\187' ] (* superscripts *) + | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) let identchar = firstchar | ['\'' '0'-'9' '@' ] let id = firstchar identchar* @@ -186,8 +193,9 @@ let symbolchar_no_brackets = (* utf-8 symbols *) '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ let symbolchar = symbolchar_no_brackets | '[' | ']' +let token_no_brackets = symbolchar_no_brackets+ let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' - +let printing_token = (token | id)+ let thm_token = "Theorem" @@ -202,6 +210,7 @@ let thm_token = let def_token = "Definition" | "Let" + | "Class" | "SubClass" | "Example" | "Local" @@ -209,11 +218,10 @@ let def_token = | "CoFixpoint" | "Record" | "Structure" + | "Instance" | "Scheme" | "Inductive" | "CoInductive" - | "Program" space+ "Definition" - | "Program" space+ "Fixpoint" let decl_token = "Hypothesis" @@ -224,6 +232,8 @@ let decl_token = let gallina_ext = "Module" + | "Include" space+ "Type" + | "Include" | "Declare" space+ "Module" | "Transparent" | "Opaque" @@ -235,6 +245,11 @@ let gallina_ext = | "Infix" | "Tactic" space+ "Notation" | "Reserved" space+ "Notation" + | "Section" + | "Context" + | "Variable" 's'? + | ("Hypothesis" | "Hypotheses") + | "End" let commands = "Pwd" @@ -254,6 +269,12 @@ let commands = | "Check" | "Type" + | "Section" + | "Chapter" + | "Variable" 's'? + | ("Hypothesis" | "Hypotheses") + | "End" + let extraction = "Extraction" | "Recursive" space+ "Extraction" @@ -261,6 +282,12 @@ let extraction = let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction +let prog_kw = + "Program" space+ gallina_kw + | "Obligation" + | "Obligations" + | "Solve" + let gallina_kw_to_hide = "Implicit" | "Ltac" @@ -275,11 +302,6 @@ let gallina_kw_to_hide = | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | "Section" - | "Chapter" - | "Variable" 's'? - | ("Hypothesis" | "Hypotheses") - | "End" | ("Set" | "Unset") space+ "Printing" space+ "Coercions" | "Declare" space+ ("Left" | "Right") space+ "Step" @@ -294,10 +316,10 @@ 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_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl +let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl +let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl +let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl (* let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" let end_verb = "(*" space* "end" space+ "verb" space* "*)" @@ -308,16 +330,16 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" (*s Scanning Coq, at beginning of line *) rule coq_bol = parse - | space* '\n'+ - { empty_line_of_code (); coq_bol lexbuf } + | space* nl+ + { Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl - { end_coq (); start_doc (); + { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in - end_doc (); start_coq (); + Output.end_doc (); Output.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 } + { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); + Output.start_coq (); coq lexbuf } | space* begin_hide { skip_hide lexbuf; coq_bol lexbuf } | space* begin_show @@ -326,28 +348,38 @@ rule coq_bol = parse { end_show (); coq_bol lexbuf } | space* gallina_kw_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 - let nbsp = count_spaces s in - indentation nbsp; - let s = String.sub s nbsp (String.length s - nbsp) in - ident s (lexeme_start lexbuf + nbsp); - let eol= body lexbuf in - if eol then coq_bol lexbuf else coq lexbuf - end } + if !Cdglobals.light && section_or_end s then + let eol = skip_to_dot lexbuf in + if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf + else + begin + let nbsp,isp = count_spaces s in + Output.indentation nbsp; + let s = String.sub s isp (String.length s - isp) in + Output.ident s (lexeme_start lexbuf + isp); + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf + end } | space* gallina_kw { let s = lexeme lexbuf in - let nbsp = count_spaces s in - let s = String.sub s nbsp (String.length s - nbsp) in - indentation nbsp; - ident s (lexeme_start lexbuf + nbsp); + let nbsp,isp = count_spaces s in + let s = String.sub s isp (String.length s - isp) in + Output.indentation nbsp; + Output.ident s (lexeme_start lexbuf + isp); let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space* "(**" space+ "printing" space+ (identifier | token) space+ + | space* prog_kw + { let s = lexeme lexbuf in + let nbsp,isp = count_spaces s in + Output.indentation nbsp; + let s = String.sub s isp (String.length s - isp) in + Output.ident s (lexeme_start lexbuf + isp); + let eol= body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + + | space* "(**" space+ "printing" space+ printing_token space+ { let tok = lexeme lexbuf in - let s = printing_token lexbuf in + let s = printing_token_body lexbuf in add_printing_token tok s; coq_bol lexbuf } | space* "(**" space+ "printing" space+ @@ -366,13 +398,13 @@ rule coq_bol = parse coq_bol lexbuf } | space* "(*" { let eol = comment lexbuf in - if eol then begin line_break(); coq_bol lexbuf end else coq lexbuf } + if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ { let eol = - if not !gallina then - begin backtrack lexbuf; indentation 0; body_bol lexbuf end + if not !Cdglobals.gallina then + begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end else skip_to_dot lexbuf in @@ -381,141 +413,148 @@ rule coq_bol = parse (*s Scanning Coq elsewhere *) and coq = parse - | "\n" - { line_break(); coq_bol lexbuf } + | nl + { Output.line_break(); coq_bol lexbuf } | "(**" space_nl - { end_coq (); start_doc (); + { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in - end_doc (); start_coq (); + Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } | "(*" { let eol = comment lexbuf in - if eol then begin line_break(); coq_bol lexbuf end + if eol then begin Output.line_break(); coq_bol lexbuf end else coq lexbuf } - | '\n'+ space* "]]" - { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end } + | nl+ space* "]]" + { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end } | eof { () } | gallina_kw_to_hide { let s = lexeme lexbuf in - if !light && section_or_end s then + if !Cdglobals.light && section_or_end s then begin let eol = skip_to_dot lexbuf in if eol then coq_bol lexbuf else coq lexbuf end else begin - ident s (lexeme_start lexbuf); + Output.ident s (lexeme_start lexbuf); let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } | gallina_kw { let s = lexeme lexbuf in - ident s (lexeme_start lexbuf); + Output.ident s (lexeme_start lexbuf); let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space+ { char ' '; coq lexbuf } + | prog_kw + { let s = lexeme lexbuf in + Output.ident s (lexeme_start lexbuf); + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } + | space+ { Output.char ' '; coq lexbuf } | eof { () } - | _ { let eol = - if not !gallina then - begin backtrack lexbuf; indentation 0; body lexbuf end + | _ { let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; Output.indentation 0; body lexbuf end else - skip_to_dot lexbuf + let eol = skip_to_dot lexbuf in + if eol then Output.line_break (); eol in if eol then coq_bol lexbuf else 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 } + | space* nl+ + { Output.paragraph (); doc_bol lexbuf } + | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')? + { let eol, lex = strip_eol (lexeme lexbuf) in + let lev, s = sec_title lex in + Output.section lev (fun () -> ignore (doc (from_string s))); + if eol then doc_bol lexbuf else doc lexbuf } + | space* '-'+ + { let n = count_dashes (lexeme lexbuf) in + if n >= 4 then Output.rule () else Output.item n; + doc lexbuf } + | "<<" space* + { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf } | eof - { false } + { true } | _ { backtrack lexbuf; doc lexbuf } (*s Scanning documentation elsewhere *) and doc = parse - | "\n" - { char '\n'; doc_bol lexbuf } + | nl + { Output.char '\n'; doc_bol lexbuf } | "[" { brackets := 1; - start_inline_coq (); escaped_coq lexbuf; end_inline_coq (); + Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); doc lexbuf } - | "[[" '\n' space* - { formatted := true; line_break (); start_inline_coq (); - indentation (count_spaces (lexeme lexbuf)); + | "[[" nl space* + { formatted := true; Output.line_break (); Output.start_inline_coq (); + Output.indentation (fst (count_spaces (lexeme lexbuf))); let eol = body_bol lexbuf in - end_inline_coq (); formatted := false; + Output.end_inline_coq (); formatted := false; if eol then doc_bol lexbuf else doc lexbuf} - | '*'* "*)" space* '\n' + | '*'* "*)" space* nl { true } | '*'* "*)" { false } | "$" - { start_latex_math (); escaped_math_latex lexbuf; doc lexbuf } + { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf } | "$$" - { char '$'; doc lexbuf } + { Output.char '$'; doc lexbuf } | "%" { escaped_latex lexbuf; doc lexbuf } | "%%" - { char '%'; doc lexbuf } + { Output.char '%'; doc lexbuf } | "#" { escaped_html lexbuf; doc lexbuf } | "##" - { char '#'; doc lexbuf } + { Output.char '#'; doc lexbuf } | eof { false } | _ - { char (lexeme_char lexbuf 0); doc lexbuf } + { Output.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 } + | "$" { Output.stop_latex_math () } + | eof { Output.stop_latex_math () } + | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf } and escaped_latex = parse | "%" { () } | eof { () } - | _ { latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } + | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } and escaped_html = parse | "#" { () } | "&#" - { html_char '&'; html_char '#'; escaped_html lexbuf } + { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf } | "##" - { html_char '#'; escaped_html lexbuf } + { Output.html_char '#'; escaped_html lexbuf } | eof { () } - | _ { html_char (lexeme_char lexbuf 0); escaped_html lexbuf } + | _ { Output.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 } + | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () } + | eof { Output.stop_verbatim () } + | _ { Output.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 } + if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end } | "[" - { incr brackets; char '['; escaped_coq lexbuf } + { incr brackets; Output.char '['; escaped_coq lexbuf } | "(*" { ignore (comment lexbuf); escaped_coq lexbuf } | "*)" @@ -524,18 +563,18 @@ and escaped_coq = parse { () } | token_brackets { let s = lexeme lexbuf in - symbol s; + Output.symbol s; escaped_coq lexbuf } | (identifier '.')* identifier - { ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } + { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } | _ - { char (lexeme_char lexbuf 0); escaped_coq lexbuf } + { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf } (*s Coq "Comments" command. *) and comments = parse | space_nl+ - { char ' '; comments lexbuf } + { Output.char ' '; comments lexbuf } | '"' [^ '"']* '"' { let s = lexeme lexbuf in let s = String.sub s 1 (String.length s - 2) in @@ -547,61 +586,79 @@ and comments = parse | eof { () } | _ - { char (lexeme_char lexbuf 0); comments lexbuf } + { Output.char (lexeme_char lexbuf 0); comments lexbuf } (*s Skip comments *) and comment = parse - | "(*" { ignore (comment lexbuf); comment lexbuf } - | "*)" space* '\n'+ { true } + | "(*" { comment lexbuf } + | "*)" space* nl { true } | "*)" { false } | eof { false } | _ { comment lexbuf } and skip_to_dot = parse - | '.' space* '\n' { true } + | '.' space* nl { true } | eof | '.' space+ { false} | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf } | _ { skip_to_dot lexbuf } and body_bol = parse | space+ - { indentation (count_spaces (lexeme lexbuf)); body lexbuf } + { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } | _ { backtrack lexbuf; body lexbuf } and body = parse - | '\n' {line_break(); body_bol lexbuf} - | '\n'+ space* "]]" - { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true } + | nl {Output.line_break(); body_bol lexbuf} + | nl+ space* "]]" + { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true } | eof { false } - | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true } - | '.' space+ { char '.'; char ' '; false } + | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true } + | '.' space+ { Output.char '.'; Output.char ' '; false } + | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf } | "(*" { let eol = comment lexbuf in - if eol then begin line_break(); body_bol lexbuf end else body lexbuf } + if eol + then begin Output.line_break(); body_bol lexbuf end + else body lexbuf } | identifier { let s = lexeme lexbuf in - ident s (lexeme_start lexbuf); + Output.ident s (lexeme_start lexbuf); body lexbuf } - | token + | token_no_brackets { let s = lexeme lexbuf in - symbol s; body lexbuf } + Output.symbol s; body lexbuf } | _ { let c = lexeme_char lexbuf 0 in - char c; + Output.char c; body lexbuf } +and notation_bol = parse + | space+ + { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf } + | _ { backtrack lexbuf; notation lexbuf } + +and notation = parse + | nl { Output.line_break(); notation_bol lexbuf } + | '"' { Output.char '"'; false } + | token + { let s = lexeme lexbuf in + Output.symbol s; notation lexbuf } + | _ { let c = lexeme_char lexbuf 0 in + Output.char c; + notation lexbuf } + and skip_hide = parse | eof | end_hide { () } | _ { skip_hide lexbuf } (*s Reading token pretty-print *) -and printing_token = parse +and printing_token_body = parse | "*)" | eof { let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } | _ { Buffer.add_string token_buffer (lexeme lexbuf); - printing_token lexbuf } + printing_token_body lexbuf } (*s Applying the scanners to files *) @@ -609,11 +666,11 @@ and printing_token = parse let coq_file f m = reset (); - Index.scan_file f m; - start_module (); + Index.current_library := m; + Output.start_module (); let c = open_in f in let lb = from_channel c in - start_coq (); coq_bol lb; end_coq (); + Output.start_coq (); coq_bol lb; Output.end_coq (); close_in c } -- cgit v1.2.3