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/coqdoc.sty | 104 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 73 insertions(+), 31 deletions(-) (limited to 'tools/coqdoc/coqdoc.sty') 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 -- cgit v1.2.3