From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- tools/coqdoc/cdglobals.ml | 3 +- tools/coqdoc/coqdoc.css | 38 ++++- tools/coqdoc/coqdoc.sty | 104 +++++++++---- tools/coqdoc/index.mli | 4 +- tools/coqdoc/index.mll | 48 ++++-- tools/coqdoc/main.ml | 24 ++- tools/coqdoc/output.ml | 365 ++++++++++++++++++++++++++++++---------------- tools/coqdoc/output.mli | 4 +- tools/coqdoc/pretty.mll | 113 +++++++++----- 9 files changed, 487 insertions(+), 216 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 3339b1db..5bcbed64 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -10,7 +10,7 @@ (*s Output options *) -type target_language = LaTeX | HTML | TeXmacs +type target_language = LaTeX | HTML | TeXmacs | Raw let target_language = ref HTML @@ -57,6 +57,7 @@ let externals = ref true let coqlib = ref "http://coq.inria.fr/library/" let coqlib_path = ref Coq_config.coqlib let raw_comments = ref false +let interpolate = ref false let charset = ref "iso-8859-1" let inputenc = ref "" diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 65c39b7a..a9a99706 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -25,7 +25,7 @@ body { padding: 0px 0px; padding: 10px; overflow: hidden; font-size: 100%; - line-height: 80% } + line-height: 100% } #main a.idref:visited {color : #416DFF; text-decoration : none; } #main a.idref:link {color : #416DFF; text-decoration : none; } @@ -43,8 +43,6 @@ body { padding: 0px 0px; #main .section { background-color:#90bdff; font-size : 175% } -#main code { font-family: monospace } - #main .doc { margin: 0px; padding: 10px; font-family: sans-serif; @@ -55,7 +53,13 @@ body { padding: 0px 0px; background-color: #90bdff; border-style: plain} -#main .doc code { font-family: monospace} +.inlinecode { + display: inline; + font-family: monospace } + +.code { + display: block; + font-family: monospace } /* Pied de page */ @@ -66,3 +70,29 @@ body { padding: 0px 0px; #footer a:link { text-decoration: none; color: #888888; } +.id { display: inline; } + +.id[type="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[type="var"] { + color: rgb(40%,0%,40%); +} + +.id[type="definition"] { + color: rgb(0%,40%,0%); +} + +.id[type="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[type="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[type="keyword"] { + color : #cf1d1d; +/* color: black; */ +} diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index d31314c5..ef4f4119 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -27,6 +27,11 @@ %HEVEA\renewcommand{\medskip}{} %HEVEA\renewcommand{\bigskip}{} + +%HEVEA\newcommand{\lnot}{\coqwkw{not}} +%HEVEA\newcommand{\lor}{\coqwkw{or}} +%HEVEA\newcommand{\land}{\&} + % own name \newcommand{\coqdoc}{\textsf{coqdoc}} @@ -39,7 +44,7 @@ \newcommand{\coqdockw}[1]{\texttt{#1}} % macro for typesetting variable identifiers -\newcommand{\coqdocid}[1]{\textit{#1}} +\newcommand{\coqdocvar}[1]{\textit{#1}} % macro for typesetting constant identifiers \newcommand{\coqdoccst}[1]{\textsf{#1}} @@ -57,52 +62,93 @@ % macro for typesetting constructor identifiers \newcommand{\coqdocconstr}[1]{\textsf{#1}} +% macro for typesetting tactic identifiers +\newcommand{\coqdoctac}[1]{\texttt{#1}} + + +% Environment encompassing code fragments +% !!! CAUTION: This environment may have empty contents +\newenvironment{coqdoccode}{}{} + % 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}} +% Base indentation length +\newlength{\coqdocbaseindent} +\setlength{\coqdocbaseindent}{0em} + +% Beginning of a line without any Coq indentation +\newcommand{\coqdocnoindent}{\noindent\kern\coqdocbaseindent} +% Beginning of a line with a given Coq indentation +\newcommand{\coqdocindent}[1]{\noindent\kern\coqdocbaseindent\noindent\kern#1} +% End-of-the-line +\newcommand{\coqdoceol}{\hspace*{\fill}\setlength\parskip{0pt}\par} +% Empty lines (in code only) +\newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em} % macro for typesetting the title of a module implementation \newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } \usepackage{ifpdf} \ifpdf - \usepackage[pdftex]{hyperref} + \RequirePackage{hyperref} \hypersetup{raiselinks=true,colorlinks=true,linkcolor=black} - \usepackage[all]{hypcap} + + % To do indexing, use something like: + % \usepackage{multind} + % \newcommand{\coqdef}[3]{\hypertarget{coq:#1}{\index{coq}{#1@#2|hyperpage}#3}} \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}}}} + \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}} \else \newcommand{\coqdef}[3]{#3} \newcommand{\coqref}[2]{#2} - \newcommand{\identref}[2]{\textsf {#2}} + \newcommand{\texorpdfstring}[2]{#1} + \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}}} - +\newif\if@coqdoccolors + \@coqdoccolorsfalse + +\DeclareOption{color}{\@coqdoccolorstrue} +\ProcessOptions + +\if@coqdoccolors +\RequirePackage{xcolor} +\definecolor{varpurple}{rgb}{0.4,0,0.4} +\definecolor{constrmaroon}{rgb}{0.6,0,0} +\definecolor{defgreen}{rgb}{0,0.4,0} +\definecolor{indblue}{rgb}{0,0,0.8} +\definecolor{kwred}{rgb}{0.8,0.1,0.1} + +\def\coqdocvarcolor{varpurple} +\def\coqdockwcolor{kwred} +\def\coqdoccstcolor{defgreen} +\def\coqdocindcolor{indblue} +\def\coqdocconstrcolor{constrmaroon} +\def\coqdocmodcolor{defgreen} +\def\coqdocaxcolor{varpurple} +\def\coqdoctaccolor{black} + +\def\coqdockw#1{{\color{\coqdockwcolor}{\texttt{#1}}}} +\def\coqdocvar#1{{\color{\coqdocvarcolor}{\textit{#1}}}} +\def\coqdoccst#1{{\color{\coqdoccstcolor}{\textrm{#1}}}} +\def\coqdocind#1{{\color{\coqdocindcolor}{\textsf{#1}}}} +\def\coqdocconstr#1{{\color{\coqdocconstrcolor}{\textsf{#1}}}} +\def\coqdocmod#1{{{\color{\coqdocmodcolor}{\textsc{\textsf{#1}}}}}} +\def\coqdocax#1{{{\color{\coqdocaxcolor}{\textsl{\textrm{#1}}}}}} +\def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}} +\fi \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{\coqvariable}[2]{\coqdocvar{#2}} +\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#2}}} \newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} @@ -133,8 +179,8 @@ \newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}} -\newcommand{\coqsection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}} -\newcommand{\coqsectionref}[2]{\coqref{#1}{\coqdoccst{#2}}} +\newcommand{\coqsection}[2]{\coqdef{sec:#1}{#2}{\coqdoccst{#2}}} +\newcommand{\coqsectionref}[2]{\coqref{sec:#1}{\coqdoccst{#2}}} %\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}} @@ -145,11 +191,7 @@ \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}} -%HEVEA\newcommand{\land}{\&} +\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}} +\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}} +\endinput diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 1da8ebd7..56a3cd11 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 11065 2008-06-06 22:39:43Z msozeau $ i*) +(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) open Cdglobals @@ -40,6 +40,8 @@ type index_entry = val find : coq_module -> loc -> index_entry +val find_string : coq_module -> string -> index_entry + val add_module : coq_module -> unit type module_kind = Local | Coqlib | Unknown diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index fc2090dc..f8adb52b 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mll 11065 2008-06-06 22:39:43Z msozeau $ i*) +(*i $Id: index.mll 11790 2009-01-15 20:19:58Z msozeau $ i*) { @@ -47,9 +47,14 @@ let current_type = ref Library let current_library = ref "" (** refers to the file being parsed *) -let table = Hashtbl.create 97 - (** [table] is used to store references and definitions *) +(** [deftable] stores only definitions and is used to interpolate idents + inside comments, which are not globalized otherwise. *) +let deftable = Hashtbl.create 97 + +(** [reftable] stores references and definitions *) +let reftable = Hashtbl.create 97 + let full_ident sp id = if sp <> "<>" then if id <> "<>" then @@ -60,15 +65,24 @@ let full_ident sp id = else "" let add_def loc ty sp id = - Hashtbl.add table (!current_library, loc) (Def (full_ident sp id, ty)) - + Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)); + Hashtbl.add deftable id (Ref (!current_library, 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)) + if Hashtbl.mem reftable (m, loc) then () + else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); + let idx = if id = "<>" then m' else id in + if Hashtbl.mem deftable idx then () + else Hashtbl.add deftable idx (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) - +let add_mod m loc m' id = + Hashtbl.add reftable (m, loc) (Mod (m', id)); + Hashtbl.add deftable m (Mod (m', id)) + +let find m l = Hashtbl.find reftable (m, l) + +let find_string m s = Hashtbl.find deftable s + (*s Manipulating path prefixes *) type stack = string list @@ -216,7 +230,7 @@ let all_entries () = | Def (s,t) -> add_g s m t; add_bt t s m | Ref _ | Mod _ -> () in - Hashtbl.iter classify table; + Hashtbl.iter classify reftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; idx_entries = sort_entries !gl; @@ -238,7 +252,9 @@ let firstchar = let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] -let ident = firstchar identchar* +let id = firstchar identchar* +let pfx_id = (id '.')* +let ident = id | pfx_id id let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" let end_hide = "(*" space* "end" space+ "hide" space* "*)" @@ -406,9 +422,9 @@ and module_refs = parse | ident { let id = lexeme lexbuf in (try - add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id - with - Not_found -> () + add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id + with + Not_found -> () ); module_refs lexbuf } | eof @@ -418,7 +434,7 @@ and module_refs = parse { let type_of_string = function - | "def" | "coe" | "subclass" | "canonstruc" + | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" | "ex" | "scheme" -> Definition | "prf" | "thm" -> Lemma | "ind" | "coind" -> Inductive diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 81560259..2e97618b 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: main.ml 11236 2008-07-18 15:58:12Z notin $ i*) +(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*) (* Modified by Lionel Elie Mamane on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -30,6 +30,7 @@ let usage () = prerr_endline " --html produce a HTML document (default)"; prerr_endline " --latex produce a LaTeX document"; prerr_endline " --texmacs produce a TeXmacs document"; + prerr_endline " --raw produce a text document"; prerr_endline " --dvi output the DVI"; prerr_endline " --ps output the PostScript"; prerr_endline " --pdf output the Pdf"; @@ -56,12 +57,14 @@ let usage () = 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 " --boot run in boot mode"; 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 " --interpolate try to typeset identifiers in comments using definitions in the same module"; prerr_endline ""; exit 1 @@ -81,6 +84,7 @@ let banner () = let target_full_name f = match !Cdglobals.target_language with | HTML -> f ^ ".html" + | Raw -> f ^ ".txt" | _ -> f ^ ".tex" (*s \textbf{Separation of files.} Files given on the command line are @@ -257,6 +261,8 @@ let parse () = Cdglobals.target_language := HTML; parse_rec rem | ("-texmacs" | "--texmacs") :: rem -> Cdglobals.target_language := TeXmacs; parse_rec rem + | ("-raw" | "--raw") :: rem -> + Cdglobals.target_language := Raw; parse_rec rem | ("-charset" | "--charset") :: s :: rem -> Cdglobals.charset := s; parse_rec rem | ("-charset" | "--charset") :: [] -> @@ -267,6 +273,9 @@ let parse () = usage () | ("-raw-comments" | "--raw-comments") :: rem -> Cdglobals.raw_comments := true; parse_rec rem + | ("-interpolate" | "--interpolate") :: rem -> + Cdglobals.interpolate := true; parse_rec rem + | ("-latin1" | "--latin1") :: rem -> Cdglobals.set_latin1 (); parse_rec rem | ("-utf8" | "--utf8") :: rem -> @@ -310,6 +319,8 @@ let parse () = Cdglobals.coqlib := u; parse_rec rem | ("--coqlib" | "-coqlib") :: [] -> usage () + | ("--boot" | "-boot") :: rem -> + Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: d :: rem -> Cdglobals.coqlib_path := d; parse_rec rem | ("--coqlib_path" | "-coqlib_path") :: [] -> @@ -318,6 +329,7 @@ let parse () = add_file (what_file f); parse_rec rem in parse_rec (List.tl (Array.to_list Sys.argv)); + Output.initialize (); List.rev !files @@ -414,10 +426,10 @@ let read_glob x = match x with | Vernac_file (f,m) -> let glob = (Filename.chop_extension f) ^ ".glob" in - (try + (try Vernac_file (f, Index.read_glob glob) - with _ -> - eprintf "Warning: file %s cannot be opened; links will not be available\n" glob; + with e -> + eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e); x) | Latex_file _ -> x @@ -430,13 +442,13 @@ let produce_document 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 (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src); (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); + if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src); (match !Cdglobals.glob_source with | NoGlob -> () | DotGlob -> ignore (List.map read_glob l) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 93414f22..c146150c 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 11154 2008-06-19 18:42:19Z msozeau $ i*) +(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*) open Cdglobals open Index @@ -32,43 +32,48 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Chapter"; "Check"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; - "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; + "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Set"; "Unset"; "Variable"; "Variables"; "Context"; + "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; - "Arguments"; "Add"; "Strict"; - "Typeclasses"; "Instance"; "Class"; "Instantiation"; + "Implicit Arguments"; "Add"; "Strict"; + "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; + "subgoal"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; - "Program Instance"; + "Program Instance"; "Equations"; "Equations_nocomp"; (*i (* coq terms *) *) - "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; - "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where" + "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; + "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; + (* Ltac *) + "before"; "after" ] let is_tactic = build_table - [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite"; - "destruct"; "induction"; "elim"; "dependent"; - "generalize"; "clear"; "rename"; "move"; "set"; "assert"; - "cut"; "assumption"; "exact"; "split"; "try"; "discriminate"; + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; + "set"; "assert"; "do"; "repeat"; + "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; "transitivity"; "replace"; "setoid_replace"; "inversion"; "inversion_clear"; - "pattern"; "intuition"; "congruence"; + "pattern"; "intuition"; "congruence"; "fail"; "fresh"; "trivial"; "exact"; "tauto"; "firstorder"; "ring"; - "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ] + "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ] (*s Current Coq module *) @@ -92,27 +97,31 @@ let find_printing_token tok = 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{|}"; - "->", "\\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}"; - (* "fun", "\\ensuremath{\\lambda}" ? *) - ] +let initialize () = + let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in + List.iter + (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l')) + [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; + "|", "\\ensuremath{|}", None; + "->", "\\ensuremath{\\rightarrow}", if_utf8 "→"; + "->~", "\\ensuremath{\\rightarrow\\lnot}", None; + "->~~", "\\ensuremath{\\rightarrow\\lnot\\lnot}", None; + "<-", "\\ensuremath{\\leftarrow}", None; + "<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔"; + "=>", "\\ensuremath{\\Rightarrow}", if_utf8 "⇒"; + "<=", "\\ensuremath{\\le}", if_utf8 "≤"; + ">=", "\\ensuremath{\\ge}", if_utf8 "≥"; + "<>", "\\ensuremath{\\not=}", if_utf8 "≠"; + "~", "\\ensuremath{\\lnot}", if_utf8 "¬"; + "/\\", "\\ensuremath{\\land}", if_utf8 "∧"; + "\\/", "\\ensuremath{\\lor}", if_utf8 "∨"; + "|-", "\\ensuremath{\\vdash}", None; + "forall", "\\ensuremath{\\forall}", if_utf8 "∀"; + "exists", "\\ensuremath{\\exists}", if_utf8 "∃"; + "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; + "λ", "\\ensuremath{\\lambda}", if_utf8 "λ" + (* "fun", "\\ensuremath{\\lambda}" ? *) + ] (*s Table of contents *) @@ -130,6 +139,9 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r module Latex = struct + let in_title = ref false + let in_doc = ref false + (*s Latex preamble *) let (preamble : string Queue.t) = Queue.create () @@ -208,7 +220,7 @@ module Latex = struct let indentation n = if n == 0 then - printf "\\noindent\n" + printf "\\coqdocnoindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space @@ -243,35 +255,49 @@ module Latex = struct 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 + printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}" let defref m id ty s = printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" + let reference s = function + | 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 "\\coqdocvar{"; raw_ident s; printf "}" + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin 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 "}") + reference s (Index.find !current_module loc) 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 else begin + if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + then + try reference s (Index.find_string !current_module s) + with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}") + else (printf "\\coqdocvar{"; raw_ident s; printf "}") + end end end - let ident s l = with_latex_printing (fun s -> ident s l) s - + let ident s l = + if !in_title then ( + printf "\\texorpdfstring{"; + with_latex_printing (fun s -> ident s l) s; + printf "}{"; raw_ident s; printf "}") + else + with_latex_printing (fun s -> ident s l) s + let symbol = with_latex_printing raw_ident let rec reach_item_level n = @@ -290,13 +316,13 @@ module Latex = struct let stop_item () = reach_item_level 0 - let start_doc () = printf "\n\n\n\\noindent\n" + let start_doc () = in_doc := true - let end_doc () = stop_item (); printf "\n\n\n" + let end_doc () = in_doc := false; stop_item () - let start_coq () = () + let start_coq () = printf "\\begin{coqdoccode}\n" - let end_coq () = () + let end_coq () = printf "\\end{coqdoccode}\n" let start_code () = end_doc (); start_coq () @@ -312,17 +338,17 @@ module Latex = struct let section lev f = stop_item (); output_string (section_kind lev); - f (); + in_title := true; f (); in_title := false; printf "}\n\n" let rule () = printf "\\par\n\\noindent\\hrulefill\\par\n\\noindent{}" - let paragraph () = stop_item (); printf "\n\n\\medskip\n" + let paragraph () = stop_item (); printf "\n\n" let line_break () = printf "\\coqdoceol\n" - let empty_line_of_code () = printf "\n\n\\medskip\n" + let empty_line_of_code () = printf "\\coqdocemptyline\n" let start_inline_coq () = () @@ -394,7 +420,8 @@ module Html = struct let line_break () = printf "
\n" - let empty_line_of_code () = printf "\n
\n" + let empty_line_of_code () = + printf "\n
\n" let char = function | '<' -> printf "<" @@ -417,49 +444,54 @@ module Html = struct 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 fid s = match find_module m with | Local -> - printf "" m fid; raw_ident s; printf "" + printf "" m; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in - printf "" m fid; raw_ident s; printf "" + printf "" m; raw_ident s; printf "" | Coqlib | Unknown -> raw_ident s + let ident_ref m fid typ s = + match find_module m with + | Local -> + printf "" typ; + printf "" m fid; raw_ident s; + printf "" + | Coqlib when !externals -> + let m = Filename.concat !coqlib m in + printf "" typ; + printf "" m fid; + raw_ident s; printf "" + | Coqlib | Unknown -> + printf "" typ; raw_ident s; printf "" + let ident s loc = if is_keyword s then begin - printf ""; + printf ""; raw_ident s; printf "" end else begin try (match Index.find !current_module loc with - | Def (fullid,_) -> - printf "" fullid; raw_ident s + | Def (fullid,ty) -> + printf "" (type_name ty); + printf "" fullid; raw_ident s; printf "" | Mod (m,s') when s = s' -> module_ref m s | Ref (m,fullid,ty) -> - ident_ref m fullid s + ident_ref m fullid (type_name ty) s | Mod _ -> - raw_ident s) + printf ""; raw_ident s ; printf "") with Not_found -> - raw_ident s + if is_tactic s then + (printf ""; raw_ident s; printf "") + else + (printf ""; raw_ident s ; printf "") end - + let with_html_printing f tok = try (match Hashtbl.find token_pp tok with @@ -488,9 +520,9 @@ module Html = struct let stop_item () = reach_item_level 0 - let start_coq () = if not !raw_comments then printf "\n" + let start_coq () = if not !raw_comments then printf "
\n" - let end_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 @@ -504,9 +536,9 @@ module Html = struct let end_code () = end_coq (); start_doc () - let start_inline_coq () = printf "" + let start_inline_coq () = printf "" - let end_inline_coq () = printf "" + let end_inline_coq () = printf "" let paragraph () = stop_item (); printf "\n

\n" @@ -539,7 +571,7 @@ module Html = struct let all_letters i = List.iter (letter_index false i.idx_name) i.idx_entries (* Construction d'une liste des index (1 index global, puis 1 - index par catégorie) *) + index par catégorie) *) let format_global_index = Index.map (fun s (m,t) -> @@ -578,7 +610,7 @@ module Html = struct printf "\n" let make_one_multi_index prt_tbl i = - (* Attn: make_one_multi_index créé un nouveau fichier... *) + (* Attn: make_one_multi_index créé un nouveau fichier... *) let idx = i.idx_name in let one_letter ((c,l) as cl) = open_out_file (sprintf "index_%s_%c.html" idx c); @@ -776,68 +808,155 @@ module TeXmacs = struct end + +(*s LaTeX output *) + +module Raw = struct + + let header () = () + + let trailer () = () + + let char = output_char + + let label_char c = match c with + | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' + | '^' | '~' -> () + | _ -> + 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 () = () + let end_module () = () + + let start_latex_math () = () + let stop_latex_math () = () + + let start_verbatim () = () + + let stop_verbatim () = () + + let indentation n = + for i = 1 to n do printf " " done + + let ident s loc = raw_ident s + + let symbol = raw_ident + + let item n = printf "- " + + let stop_item () = () + + let start_doc () = printf "(** " + let end_doc () = printf " *)\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 -> "*" + | 2 -> "**" + | 3 -> "***" + | 4 -> "****" + | _ -> assert false + + let section lev f = + output_string (section_kind lev); + f () + + let rule () = () + + let paragraph () = printf "\n\n" + + let line_break () = printf "\n" + + let empty_line_of_code () = printf "\n" + + let start_inline_coq () = () + let end_inline_coq () = () + + let make_multi_index () = () + 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 select f1 f2 f3 f4 x = + match !target_language with LaTeX -> f1 x | HTML -> f2 x | TeXmacs -> f3 x | Raw -> f4 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 header = select Latex.header Html.header TeXmacs.header Raw.header +let trailer = select Latex.trailer Html.trailer TeXmacs.trailer Raw.trailer let start_module = - select Latex.start_module Html.start_module TeXmacs.start_module + select Latex.start_module Html.start_module TeXmacs.start_module Raw.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_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc +let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.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_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq +let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.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_code = select Latex.start_code Html.start_code TeXmacs.start_code Raw.start_code +let end_code = select Latex.end_code Html.end_code TeXmacs.end_code Raw.end_code let start_inline_coq = - select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq + select Latex.start_inline_coq Html.start_inline_coq TeXmacs.start_inline_coq Raw.start_inline_coq let end_inline_coq = - select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq + select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.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 indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation +let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph +let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break let empty_line_of_code = select - Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code + Latex.empty_line_of_code Html.empty_line_of_code TeXmacs.empty_line_of_code Raw.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 section = select Latex.section Html.section TeXmacs.section Raw.section +let item = select Latex.item Html.item TeXmacs.item Raw.item +let stop_item = select Latex.stop_item Html.stop_item TeXmacs.stop_item Raw.stop_item +let rule = select Latex.rule Html.rule TeXmacs.rule Raw.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 char = select Latex.char Html.char TeXmacs.char Raw.char +let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident +let symbol = select Latex.symbol Html.symbol TeXmacs.symbol Raw.symbol -let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char +let latex_char = select Latex.latex_char Html.latex_char TeXmacs.latex_char Raw.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 + select Latex.latex_string Html.latex_string TeXmacs.latex_string Raw.latex_string +let html_char = select Latex.html_char Html.html_char TeXmacs.html_char Raw.html_char let html_string = - select Latex.html_string Html.html_string TeXmacs.html_string + select Latex.html_string Html.html_string TeXmacs.html_string Raw.html_string let start_latex_math = - select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math + select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = - select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math + select Latex.stop_latex_math Html.stop_latex_math TeXmacs.stop_latex_math Raw.stop_latex_math let start_verbatim = - select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim + select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim let stop_verbatim = - select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim + select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim let verbatim_char = - select output_char Html.char TeXmacs.char + select output_char Html.char TeXmacs.char Raw.char let hard_verbatim_char = output_char -let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index -let make_index = select Latex.make_index Html.make_index TeXmacs.make_index -let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc +let make_multi_index = select Latex.make_multi_index Html.make_multi_index TeXmacs.make_multi_index Raw.make_multi_index +let make_index = select Latex.make_index Html.make_index TeXmacs.make_index Raw.make_index +let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc Raw.make_toc diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 87b311f3..3da80335 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -6,11 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*) +(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) open Cdglobals open Index +val initialize : unit -> unit + val add_printing_token : string -> string option * string option -> unit val remove_printing_token : string -> unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index baace5ba..3ae5cbed 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*) +(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*) (*s Utility functions for the scanners *) @@ -57,6 +57,7 @@ let formatted = ref false let brackets = ref 0 let comment_level = ref 0 + let in_proof = ref false let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos @@ -173,11 +174,12 @@ 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 *) - '\206' ['\177'-'\183'] | + '\206' ('\160' | [ '\177'-'\183'] | '\187') | '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) | '\129' [ '\176'-'\187' ] (* superscripts *) | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) @@ -188,17 +190,24 @@ let pfx_id = (id '.')* let identifier = id | pfx_id id -let symbolchar_no_brackets = - ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' - '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' - '{' '}' '(' ')'] | +let symbolchar_symbol_no_brackets = + ['!' '$' '%' '&' '*' '+' ',' '^' '#' + '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] | (* utf-8 symbols *) '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ +let symbolchar_no_brackets = symbolchar_symbol_no_brackets | + [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_'] let symbolchar = symbolchar_no_brackets | '[' | ']' -let token_no_brackets = symbolchar_no_brackets+ -let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' +let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets* +let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']' let printing_token = (token | id)+ +(* tokens with balanced brackets *) +let token_brackets = + ( token_no_brackets ('[' token_no_brackets? ']')* + | token_no_brackets? ('[' token_no_brackets? ']')+ ) + token_no_brackets? + let thm_token = "Theorem" | "Lemma" @@ -208,22 +217,26 @@ let thm_token = | "Proposition" | "Property" | "Goal" + | "Next" space+ "Obligation" let def_token = "Definition" | "Let" | "Class" - | "SubClass" + | "SubClass" | "Example" | "Local" | "Fixpoint" + | "Boxed" | "CoFixpoint" | "Record" | "Structure" - | "Instance" | "Scheme" | "Inductive" | "CoInductive" + | "Equations" + | "Instance" + | "Global" space+ "Instance" let decl_token = "Hypothesis" @@ -277,6 +290,8 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" +let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort" + let extraction = "Extraction" | "Recursive" space+ "Extraction" @@ -291,7 +306,8 @@ let prog_kw = | "Solve" let gallina_kw_to_hide = - "Implicit" + "Implicit" space+ "Arguments" + | "Next" "Obligation" | "Ltac" | "Require" | "Import" @@ -308,12 +324,6 @@ let gallina_kw_to_hide = | "Declare" space+ ("Left" | "Right") space+ "Step" -(* 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 = " " @@ -333,7 +343,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" rule coq_bol = parse | space* nl+ - { Output.empty_line_of_code (); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -352,7 +362,7 @@ rule coq_bol = parse { let s = lexeme lexbuf in 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 + if eol then (coq_bol lexbuf) else coq lexbuf else begin let nbsp,isp = count_spaces s in @@ -362,8 +372,35 @@ rule coq_bol = parse let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } - | space* gallina_kw + | space* thm_token { let s = lexeme lexbuf in + 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 + in_proof := true; + if eol then coq_bol lexbuf else coq lexbuf } + | space* "Proof" (space* "." | space+ "with") + { in_proof := true; + let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; body_bol lexbuf end + else true + in if eol then coq_bol lexbuf else coq lexbuf } + | space* end_kw { + let eol = + if not (!in_proof && !Cdglobals.gallina) then + begin backtrack lexbuf; body_bol lexbuf end + else + skip_to_dot lexbuf + in + in_proof := false; + if eol then coq_bol lexbuf else coq lexbuf } + | space* gallina_kw + { + in_proof := false; + let s = lexeme lexbuf in let nbsp,isp = count_spaces s in let s = String.sub s isp (String.length s - isp) in Output.indentation nbsp; @@ -371,7 +408,9 @@ rule coq_bol = parse let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } | space* prog_kw - { let s = lexeme lexbuf in + { + in_proof := false; + 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 @@ -409,7 +448,7 @@ rule coq_bol = parse | _ { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end + begin backtrack lexbuf; body_bol lexbuf end else skip_to_dot lexbuf in @@ -419,7 +458,7 @@ rule coq_bol = parse and coq = parse | nl - { Output.line_break(); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf } | "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -448,6 +487,15 @@ and coq = parse let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } + | end_kw { + let eol = + if not (!in_proof && !Cdglobals.gallina) then + begin backtrack lexbuf; body lexbuf end + else + skip_to_dot lexbuf + in + in_proof := false; + if eol then coq_bol lexbuf else coq lexbuf } | gallina_kw { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); @@ -463,7 +511,7 @@ and coq = parse { () } | _ { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body lexbuf end + begin backtrack lexbuf; body lexbuf end else let eol = skip_to_dot lexbuf in if eol then Output.line_break (); eol @@ -496,16 +544,15 @@ and doc_bol = parse and doc = parse | nl { Output.char '\n'; doc_bol lexbuf } - | "[" - { brackets := 1; - Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); - doc lexbuf } - | "[[" nl space* + | "[[" nl { formatted := true; Output.line_break (); Output.start_inline_coq (); - Output.indentation (fst (count_spaces (lexeme lexbuf))); let eol = body_bol lexbuf in Output.end_inline_coq (); formatted := false; if eol then doc_bol lexbuf else doc lexbuf} + | "[" + { brackets := 1; + Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); + doc lexbuf } | '*'* "*)" space* nl { true } | '*'* "*)" @@ -612,7 +659,7 @@ and skip_to_dot = parse and body_bol = parse | space+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } - | _ { backtrack lexbuf; body lexbuf } + | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } and body = parse | nl {Output.line_break(); body_bol lexbuf} @@ -645,7 +692,7 @@ and notation_bol = parse and notation = parse | nl { Output.line_break(); notation_bol lexbuf } - | '"' { Output.char '"'; false } + | '"' { Output.char '"'} | token { let s = lexeme lexbuf in Output.symbol s; notation lexbuf } @@ -660,7 +707,7 @@ and skip_hide = parse (*s Reading token pretty-print *) and printing_token_body = parse - | "*)" | eof + | "*)" nl? | eof { let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } -- cgit v1.2.3