aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-12-06 18:53:22 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-12-06 18:53:22 +0100
commit7af1b3e08452c3bbced6ca7eece2c91c6bf29137 (patch)
tree9ab4576c847a62abba67818a8785b24a7144843c /doc
parent227ff6a46ad511ff2ab0ba1ffb9017bdb0291a58 (diff)
Fix broken documentation in presence of \zeroone{... \tt ...}.
The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there.
Diffstat (limited to 'doc')
-rw-r--r--doc/common/macros.tex3
-rw-r--r--doc/refman/RefMan-tac.tex2
2 files changed, 3 insertions, 2 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index df5ee405f..5abdecfc1 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -72,7 +72,8 @@
%\newcommand{\spec}[1]{\{\,#1\,\}}
% Building regular expressions
-\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
+\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}}
+\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
%\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
%\newcommand{\onemany}[1]{$\{$#1$\}$+}
\newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 4b0652031..3f1241186 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -114,7 +114,7 @@ following syntax:
\begin{tabular}{lcl}
{\occclause} & ::= & {\tt in} {\occgoalset} \\
{\occgoalset} & ::= &
- \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+ \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
& & {\dots} {\tt ,}\\
& & {\ident$_m$} \zeroone{\atoccurrences}}\\
& & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\