diff options
| -rw-r--r-- | CHANGES | 17 | ||||
| -rw-r--r-- | doc/refman/coqdoc.tex | 134 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 11 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 2 |
5 files changed, 134 insertions, 32 deletions
@@ -49,6 +49,23 @@ Tools - New coqtop/coqc option -compat X.Y to simulate the general behavior of previous versions of Coq (provides e.g. support for 8.2 compatibility). +Coqdoc + +- List have been revamped. List depth and scope is now determined by + an "offside" whitespace rule. +- Text may be italicized by placing it in _underscores_. +- The "--index <string>" flag changes the filename of the index. +- The "--toc-depth <int>" flag limits the depth of headers which are + included in the table of contents. +- The "--lib-name <string>" flag prints "<string> Foo" instead of + "Library Foo" where library titles are called for. The + "--no-lib-name" flag eliminates the extra title. +- New option "--parse-comments" to allow parsing of regular ("(* *)") + comments. +- New option "--plain-comments" to disable interpretation inside comments. +- New option "--interpolate" to try and typeset identifiers in Coq escapings + using the available globalization information. + Library - Use "Coq standard" names for the properties of eq and identity diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 0e3cab3e6..626593fc9 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -118,22 +118,40 @@ Example: \paragraph{Lists.} -List items are introduced by 1 to 4 leading dashes. -Deepness of the list is indicated by the number of dashes. -List ends with a blank line. +List items are introduced by a leading dash. \coqdoc\ uses whitespace +to determine the depth of a new list item and which text belongs in +which list items. A list ends when a line of text starts at or before +the level of indenting of the list's dash. A list item's dash must +always be the first non-space character on its line (so, in +particular, a list can not begin on the first line of a comment - +start it on the second line instead). + Example: \begin{verbatim} - This module defines - - the predecessor [pred] - - the addition [plus] - - order relations: - -- less or equal [le] - -- less [lt] + We go by induction on [n]: + - If [n] is 0... + - If [n] is [S n'] we require... + + two paragraphs of reasoning, and two subcases: + + - In the first case... + - In the second case... + + So the theorem holds. \end{verbatim} \paragraph{Rules.} More than 4 leading dashes produce an horizontal rule. +\paragraph{Emphasis.} +Text can be italicized by placing it in underscores. A non-identifier +character must precede the leading underscore and follow the trailing +underscore, so that uses of underscores in names aren't mistaken for +emphasis. Usually, these are spaces or punctuation. + +\begin{verbatim} + This sentence contains some _emphasized text_. +\end{verbatim} \paragraph{Escapings to \LaTeX\ and HTML.} Pure \LaTeX\ or HTML material can be inserted using the following @@ -166,14 +184,14 @@ Here is the corresponding caml code: Hyperlinks can be inserted into the HTML output, so that any identifier is linked to the place of its definition. -In order to get hyperlinks you need to first compile your \Coq\ file -using \texttt{coqc \mm{}dump-glob \emph{file}}; this appends -\Coq\ names resolutions done during the compilation to file -\texttt{\emph{file}}. Take care of erasing this file, if any, when -starting the whole compilation process. +\texttt{coqc \emph{file}.v} automatically dumps localization information +in \texttt{\emph{file}.glob} or appends it to a file specified using option +\texttt{\mm{}dump-glob \emph{file}}. Take care of erasing this global file, if +any, when starting the whole compilation process. -Then invoke \texttt{coqdoc \mm{}glob-from \emph{file}} to tell -\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}}. +Then invoke \texttt{coqdoc} or \texttt{coqdoc \mm{}glob-from \emph{file}} to tell +\coqdoc\ to look for name resolutions into the file \texttt{\emph{file}} +(it will look in \texttt{\emph{file}.glob} by default). Identifiers from the \Coq\ standard library are linked to the \Coq\ web site at \url{http://coq.inria.fr/library/}. This behavior can be @@ -279,16 +297,6 @@ suffix \verb!.tex!. directory (option \texttt{-d} does not change the filename specified with option \texttt{-o}, if any). -\item[\texttt{-s }, \texttt{\mm{}short}] ~\par - - Do not insert titles for the files. The default behavior is to - insert a title like ``Library Foo'' for each file. - -\item[\texttt{-t }\textit{string}, - \texttt{\mm{}title }\textit{string}] ~\par - - Set the document title. - \item[\texttt{\mm{}body-only}] ~\par Suppress the header and trailer of the final document. Thus, you can @@ -325,7 +333,7 @@ suffix \verb!.tex!. \end{description} -\paragraph{Index options} ~\par +\paragraph{Index options} Default behavior is to build an index, for the HTML output only, into \texttt{index.html}. @@ -341,9 +349,14 @@ Default behavior is to build an index, for the HTML output only, into Generate one page for each category and each letter in the index, together with a top page \texttt{index.html}. +\item[\texttt{\mm{}index }\textit{string}] ~\par + + Make the filename of the index \textit{string} instead of ``index''. + Useful since ``index.html'' is special. + \end{description} -\paragraph{Table of contents option} ~\par +\paragraph{Table of contents option} \begin{description} @@ -354,6 +367,11 @@ Default behavior is to build an index, for the HTML output only, into beginning of the document. For a HTML output, it builds a table of contents into \texttt{toc.html}. +\item[\texttt{\mm{}toc-depth }\textit{int}] ~\par + + Only include headers up to depth \textit{int} in the table of + contents. + \end{description} \paragraph{Hyperlinks options} @@ -384,6 +402,40 @@ Default behavior is to build an index, for the HTML output only, into \end{description} +\paragraph{Title options} +\begin{description} +\item[\texttt{-s }, \texttt{\mm{}short}] ~\par + + Do not insert titles for the files. The default behavior is to + insert a title like ``Library Foo'' for each file. + +\item[\texttt{\mm{}lib-name }\textit{string}] ~\par + + Print ``\textit{string} Foo'' instead of ``Library Foo'' in titles. + For example ``Chapter'' and ``Module'' are reasonable choices. + +\item[\texttt{\mm{}no-lib-name}] ~\par + + Print just ``Foo'' instead of ``Library Foo'' in titles. + +\item[\texttt{\mm{}lib-subtitles}] ~\par + + Look for library subtitles. When enabled, the beginning of each + file is checked for a comment of the form: +\begin{alltt} +(** * ModuleName : text *) +\end{alltt} + where \texttt{ModuleName} must be the name of the file. If it is + present, the \texttt{text} is used as a subtitle for the module in + appropriate places. + +\item[\texttt{-t }\textit{string}, + \texttt{\mm{}title }\textit{string}] ~\par + + Set the document title. + +\end{description} + \paragraph{Contents options} \begin{description} @@ -408,7 +460,25 @@ The behavior of options \texttt{-g} and \texttt{-l} can be locally overridden using the \texttt{(* begin show *)} \dots\ \texttt{(* end show *)} environment (see above). -\paragraph{Language options} ~\par +There are a few options to drive the parsing of comments: +\begin{description} +\item[\texttt{\mm{}parse-comments}] ~\par + + Parses regular comments delimited by \texttt{(*} and \texttt{*)} as + well. They are typeset inline. + +\item[\texttt{\mm{}plain-comments}] ~\par + + Do not interpret comments, simply copy them as plain-text. + +\item[\texttt{\mm{}interpolate}] ~\par + + Use the globalization information to typeset identifiers appearing in + \Coq{} escapings inside comments. +\end{description} + + +\paragraph{Language options} Default behavior is to assume ASCII 7 bits input files. @@ -448,11 +518,15 @@ into your own preamble the command \begin{quote} \verb|\usepackage{coqdoc}| \end{quote} + +The package optionally takes the argument \verb|[color]| to typeset +identifiers with colors (this requires the \verb|xcolor| package). + Then you may alter the rendering of the document by redefining some macros: \begin{description} -\item[\texttt{coqdockw}, \texttt{coqdocid}] ~ +\item[\texttt{coqdockw}, \texttt{coqdocid}, \ldots] ~ The one-argument macros for typesetting keywords and identifiers. Defaults are sans-serif for keywords and italic for identifiers. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 3ad900050..065b72e7b 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -780,7 +780,7 @@ and doc indents = parse | None -> doc_bol lexbuf else doc indents lexbuf)} | "[]" - { Output.symbol "PROOFBOX"; doc indents lexbuf } + { Output.proofbox (); doc indents lexbuf } | "[" { if !Cdglobals.plain_comments then Output.char '[' else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 11a821b7c..b2e6bbd99 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -131,7 +131,6 @@ let initialize () = "exists", "\\ensuremath{\\exists}", if_utf8 "∃"; "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"; - "PROOFBOX", "\\ensuremath{\\Box}", Some "<font size=-2>☐</font>"; (* FIX THIS *) (* "fun", "\\ensuremath{\\lambda}" ? *) ] @@ -318,6 +317,8 @@ module Latex = struct let symbol s = with_latex_printing raw_ident s + let proofbox () = printf "\\ensuremath{\\Box}" + let rec reach_item_level n = if !item_level < n then begin printf "\n\\begin{itemize}\n\\item "; incr item_level; @@ -548,6 +549,8 @@ module Html = struct let symbol s = with_html_printing raw_ident s + let proofbox () = printf "<font size=-2>☐</font>" + let rec reach_item_level n = if !item_level < n then begin printf "<ul>\n<li>"; incr item_level; @@ -810,6 +813,8 @@ module TeXmacs = struct let symbol s = if !in_doc then symbol_true s else raw_ident s + let proofbox () = printf "QED" + let rec reach_item_level n = if !item_level < n then begin printf "\n<\\itemize>\n<item>"; incr item_level; @@ -921,6 +926,8 @@ module Raw = struct let symbol s = raw_ident s + let proofbox () = printf "[]" + let item n = printf "- " let stop_item () = () let reach_item_level _ = () @@ -1017,6 +1024,8 @@ 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 proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox + 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 Raw.latex_string diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 6e3f6e88b..35f056d94 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -61,6 +61,8 @@ val char : char -> unit val ident : string -> loc -> unit val symbol : string -> unit +val proofbox : unit -> unit + val latex_char : char -> unit val latex_string : string -> unit val html_char : char -> unit |