From c0adc36c5b0ca00a8db16f38feb45e20fc00fb22 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 22 Oct 2008 16:31:10 +0000 Subject: Various coqdoc improvements: - New "color" option to the coqdoc latex style file to typeset using the xcolor package, still following the McBride convention. - Work on proper indentation and spacing of output code and allow users to customise indentation (setting a base indentation length) and line skips for empty lines of code. - Also add new environments to distinguish code and documentation, doing nothing right now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11491 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/stdlib/Library.tex | 2 +- tools/coqdoc/coqdoc.sty | 92 ++++++++++++++++++++++++++++++++++++------------- tools/coqdoc/output.ml | 37 +++++++++++--------- tools/coqdoc/pretty.mll | 40 ++++++++++++++------- 4 files changed, 117 insertions(+), 54 deletions(-) diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index 8735bc720..8a5c7ab76 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -3,7 +3,7 @@ \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \usepackage{fullpage} -\usepackage{../../coqdoc} +\usepackage[color]{../../coqdoc} \input{../common/version} \input{../common/title} diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index d31314c5e..0674c8b15 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,13 +62,31 @@ % macro for typesetting constructor identifiers \newcommand{\coqdocconstr}[1]{\textsf{#1}} +% macro for typesetting tactic identifiers +\newcommand{\coqdoctac}[1]{\texttt{#1}} + + +% Environment encompassing code fragments +\newenvironment{coqdoccode}{}{} +% Environment encompassing documentation fragments +\newenvironment{coqdocdoc}{}{} + +% !!! CAUTION: These environments may have empty contents + % 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}{} @@ -74,11 +97,15 @@ \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 \coqdoccst{#2}}}} \else \newcommand{\coqdef}[3]{#3} \newcommand{\coqref}[2]{#2} @@ -87,22 +114,43 @@ \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{kwred} + +\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{kw}}}} +\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{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}} \newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}} @@ -148,8 +196,4 @@ \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}{\&} - +\endinput diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 34c993296..0d5b5e2a5 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -39,15 +39,15 @@ let is_keyword = "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"; "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"; @@ -62,17 +62,18 @@ let is_keyword = let is_tactic = build_table - [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "injection"; + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; - "destruct"; "destruction"; "destruct_call"; "induction"; "elim"; "dependent"; - "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "clear"; "rename"; "move"; "set"; "assert"; + "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; + "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; + "set"; "assert"; "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"; "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 *) @@ -116,8 +117,10 @@ let initialize () = "\\/", "\\ensuremath{\\lor}", if_utf8 "∨"; "|-", "\\ensuremath{\\vdash}", None; "forall", "\\ensuremath{\\forall}", if_utf8 "∀"; - "exists", "\\ensuremath{\\exists}", if_utf8 "∃" - (* "fun", "\\ensuremath{\\lambda}" ? *) + "exists", "\\ensuremath{\\exists}", if_utf8 "∃"; + "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; + "λ", "\\ensuremath{\\lambda}", if_utf8 "λ" + (* "fun", "\\ensuremath{\\lambda}" ? *) ] (*s Table of contents *) @@ -214,7 +217,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 @@ -262,7 +265,7 @@ module Latex = struct | Ref (m,fullid,typ) -> ident_ref m fullid typ s | Mod _ -> - printf "\\coqdocid{"; raw_ident s; printf "}" + printf "\\coqdocvar{"; raw_ident s; printf "}" let ident s loc = if is_keyword s then begin @@ -303,13 +306,13 @@ module Latex = struct let stop_item () = reach_item_level 0 - let start_doc () = printf "\n\n\n\\noindent\n" + let start_doc () = printf "\\begin{coqdocdoc}\n" - let end_doc () = stop_item (); printf "\n\n\n" + let end_doc () = stop_item (); printf "\\end{coqdocdoc}\n" - 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 () @@ -331,11 +334,11 @@ module Latex = struct 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 () = () diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index d38a09bd6..c427cc6ff 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -217,6 +217,7 @@ let thm_token = | "Proposition" | "Property" | "Goal" + | "Next Obligation" let def_token = "Definition" @@ -229,11 +230,12 @@ let def_token = | "CoFixpoint" | "Record" | "Structure" - | "Instance" | "Scheme" | "Inductive" | "CoInductive" | "Equations" + | "Instance" + | "Global Instance" let decl_token = "Hypothesis" @@ -304,6 +306,7 @@ let prog_kw = let gallina_kw_to_hide = "Implicit" space+ "Arguments" + | "Next" "Obligation" | "Ltac" | "Require" | "Import" @@ -315,7 +318,6 @@ let gallina_kw_to_hide = | "Delimit" | "Transparent" | "Opaque" - | "Proof" space+ "with" | ("Declare" space+ ("Morphism" | "Step") ) | ("Set" | "Unset") space+ "Printing" space+ "Coercions" | "Declare" space+ ("Left" | "Right") space+ "Step" @@ -379,22 +381,25 @@ rule coq_bol = parse in_proof := true; if eol then coq_bol lexbuf else coq lexbuf } | space* "Proof" (space* "." | space+ "with") - { let eol = + { in_proof := true; + 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 true in if eol then coq_bol lexbuf else coq lexbuf } | space* end_kw { - in_proof := false; let eol = - if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end + 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 - { let s = lexeme lexbuf in + { + 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; @@ -402,7 +407,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 @@ -440,7 +447,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 @@ -479,6 +486,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); @@ -494,7 +510,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 @@ -642,7 +658,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} -- cgit v1.2.3