New \grammartoken markup, similar to \token but allowed everywhere.

This commit is contained in:
Fred Drake 2001-08-20 21:36:38 +00:00
parent 2a274a7e41
commit 16bb41934c
2 changed files with 6 additions and 0 deletions

View File

@ -716,6 +716,10 @@ sub do_cmd_token{
return "<a href=\"$target\">$token</a>" . $_;
}
sub do_cmd_grammartoken{
return do_cmd_token(@_);
}
sub do_env_productionlist{
local($_) = @_;
my $lang = next_optional_argument();

View File

@ -867,11 +867,13 @@
\newcommand{\citetitle}[2][URL]{\emph{#2}}
\newcommand{\grammartoken}[1]{\texttt{#1}}
\newenvironment{productionlist}[1][\py@badkey]{
\def\optional##1{{\Large[}##1{\Large]}}
\def\production##1##2{\code{##1}&::=&\code{##2}\\}
\def\orgroup##1{{\def\or{\textbar\ }##1}}
\def\token##1{##1}
\let\grammartoken=\token
\begin{center}
\begin{tabular}{lcl}
}{%