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

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}<BR>\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}