1 files changed, 73 insertions, 31 deletions
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}<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}{}
 }
 \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