Isabelle_DOF/examples/scholarly_paper/2021-ITP-PMTI/output/document/comment.sty

279 lines
9.0 KiB
TeX

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Comment.sty version 3.6, October 1999
%
% Purpose:
% selectively in/exclude pieces of text: the user can define new
% comment versions, and each is controlled separately.
% Special comments can be defined where the user specifies the
% action that is to be taken with each comment line.
%
% Author
% Victor Eijkhout
% Department of Computer Science
% University of Tennessee
% 107 Ayres Hall
% Knoxville TN 37996
% USA
%
% victor@eijkhout.net
%
% This program is free software; you can redistribute it and/or
% modify it under the terms of the GNU General Public License
% as published by the Free Software Foundation; either version 2
% of the License, or (at your option) any later version.
%
% This program is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
% GNU General Public License for more details.
%
% For a copy of the GNU General Public License, write to the
% Free Software Foundation, Inc.,
% 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA,
% or find it on the net, for instance at
% http://www.gnu.org/copyleft/gpl.html
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This style can be used with plain TeX or LaTeX, and probably
% most other packages too.
%
% Usage: all text included between
% \comment ... \endcomment
% or \begin{comment} ... \end{comment}
% is discarded.
%
% The opening and closing commands should appear on a line
% of their own. No starting spaces, nothing after it.
% This environment should work with arbitrary amounts
% of comment, and the comment can be arbitrary text.
%
% Other `comment' environments are defined by
% and are selected/deselected with
% \includecomment{versiona}
% \excludecoment{versionb}
%
% These environments are used as
% \versiona ... \endversiona
% or \begin{versiona} ... \end{versiona}
% with the opening and closing commands again on a line of
% their own.
%
% LaTeX users note: for an included comment, the
% \begin and \end lines act as if they don't exist.
% In particular, they don't imply grouping, so assignments
% &c are not local.
%
% Special comments are defined as
% \specialcomment{name}{before commands}{after commands}
% where the second and third arguments are executed before
% and after each comment block. You can use this for global
% formatting commands.
% To keep definitions &c local, you can include \begingroup
% in the `before commands' and \endgroup in the `after commands'.
% ex:
% \specialcomment{smalltt}
% {\begingroup\ttfamily\footnotesize}{\endgroup}
% You do *not* have to do an additional
% \includecomment{smalltt}
% To remove 'smalltt' blocks, give \excludecomment{smalltt}
% after the definition.
%
% Processing comments can apply processing to each line.
% \processcomment{name}{each-line commands}%
% {before commands}{after commands}
% By defining a control sequence
% \def\Thiscomment##1{...} in the before commands the user can
% specify what is to be done with each comment line.
% BUG this does not work quite yet BUG
%
% Trick for short in/exclude macros (such as \maybe{this snippet}):
%\includecomment{cond}
%\newcommand{\maybe}[1]{}
%\begin{cond}
%\renewcommand{\maybe}[1]{#1}
%\end{cond}
%
% Basic approach of the implementation:
% to comment something out, scoop up every line in verbatim mode
% as macro argument, then throw it away.
% For inclusions, in LaTeX the block is written out to
% a file \CommentCutFile (default "comment.cut"), which is
% then included.
% In plain TeX (and other formats) both the opening and
% closing comands are defined as noop.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Changes in version 3.1
% - updated author's address
% - cleaned up some code
% - trailing contents on \begin{env} line is always discarded
% even if you've done \includecomment{env}
% - comments no longer define grouping!! you can even
% \includecomment{env}
% \begin{env}
% \begin{itemize}
% \end{env}
% Isn't that something ...
% - included comments are written to file and input again.
% Changes in 3.2
% - \specialcomment brought up to date (thanks to Ivo Welch).
% Changes in 3.3
% - updated author's address again
% - parametrised \CommentCutFile
% Changes in 3.4
% - added GNU public license
% - added \processcomment, because Ivo's fix (above) brought an
% inconsistency to light.
% Changes in 3.5
% - corrected typo in header.
% - changed author email
% - corrected \specialcomment yet again.
% - fixed excludecomment of an earlier defined environment.
% Changes in 3.6
% - The 'cut' file is now written more verbatim, using \meaning;
% some people reported having trouble with ISO latin 1, or umlaute.sty.
% - removed some \newif statements.
% Has this suddenly become \outer again?
%
% Known bugs:
% - excludecomment leads to one superfluous space
% - processcomment leads to a superfluous line break
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\makeinnocent#1{\catcode`#1=12 }
\def\csarg#1#2{\expandafter#1\csname#2\endcsname}
\def\latexname{lplain}\def\latexename{LaTeX2e}
\newwrite\CommentStream
\def\CommentCutFile{comment.cut}
\def\ProcessComment#1% start it all of
{\begingroup
\def\CurrentComment{#1}%
\let\do\makeinnocent \dospecials
\makeinnocent\^^L% and whatever other special cases
\endlinechar`\^^M \catcode`\^^M=12 \xComment}
%\def\ProcessCommentWithArg#1#2% to be used in \leveledcomment
% {\begingroup
% \def\CurrentComment{#1}%
% \let\do\makeinnocent \dospecials
% \makeinnocent\^^L% and whatever other special cases
% \endlinechar`\^^M \catcode`\^^M=12 \xComment}
{\catcode`\^^M=12 \endlinechar=-1 %
\gdef\xComment#1^^M{%
\expandafter\ProcessCommentLine}
\gdef\ProcessCommentLine#1^^M{\def\test{#1}
\csarg\ifx{End\CurrentComment Test}\test
\edef\next{\noexpand\EndOfComment{\CurrentComment}}%
\else \ThisComment{#1}\let\next\ProcessCommentLine
\fi \next}
}
\def\CSstringmeaning#1{\expandafter\CSgobblearrow\meaning#1}
\def\CSstringcsnoescape#1{\expandafter\CSgobbleescape\string#1}
{\escapechar-1
\expandafter\expandafter\expandafter\gdef
\expandafter\expandafter\expandafter\CSgobblearrow
\expandafter\string\csname macro:->\endcsname{}
}
\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi}
\def\WriteCommentLine#1{\def\CStmp{#1}%
\immediate\write\CommentStream{\CSstringmeaning\CStmp}}
% 3.1 change: in LaTeX and LaTeX2e prevent grouping
\if 0%
\ifx\fmtname\latexename
0%
\else \ifx\fmtname\latexname
0%
\else
1%
\fi \fi
%%%%
%%%% definitions for LaTeX
%%%%
\def\AfterIncludedComment
{\immediate\closeout\CommentStream
\input{\CommentCutFile}\relax
}%
\def\TossComment{\immediate\closeout\CommentStream}
\def\BeforeIncludedComment
{\immediate\openout\CommentStream=\CommentCutFile
\let\ThisComment\WriteCommentLine}
\def\includecomment
#1{\message{Include comment '#1'}%
\csarg\let{After#1Comment}\AfterIncludedComment
\csarg\def{#1}{\BeforeIncludedComment
\ProcessComment{#1}}%
\CommentEndDef{#1}}
\long\def\specialcomment
#1#2#3{\message{Special comment '#1'}%
% note: \AfterIncludedComment does \input, so #2 goes here!
\csarg\def{After#1Comment}{#2\AfterIncludedComment#3}%
\csarg\def{#1}{\BeforeIncludedComment\relax
\ProcessComment{#1}}%
\CommentEndDef{#1}}
\long\def\processcomment
#1#2#3#4{\message{Lines-Processing comment '#1'}%
\csarg\def{After#1Comment}{#3\AfterIncludedComment#4}%
\csarg\def{#1}{\BeforeIncludedComment#2\relax
\ProcessComment{#1}}%
\CommentEndDef{#1}}
\def\leveledcomment
#1#2{\message{Include comment '#1' up to level '#2'}%
%\csname #1IsLeveledCommenttrue\endcsname
\csarg\let{After#1Comment}\AfterIncludedComment
\csarg\def{#1}{\BeforeIncludedComment
\ProcessCommentWithArg{#1}}%
\CommentEndDef{#1}}
\else
%%%%
%%%%plain TeX and other formats
%%%%
\def\includecomment
#1{\message{Including comment '#1'}%
\csarg\def{#1}{}%
\csarg\def{end#1}{}}
\long\def\specialcomment
#1#2#3{\message{Special comment '#1'}%
\csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2%
\ProcessComment{#1}}%
\CommentEndDef{#1}}
\fi
%%%%
%%%% general definition of skipped comment
%%%%
\def\excludecomment
#1{\message{Excluding comment '#1'}%
\csarg\def{#1}{\let\AfterComment\relax
\def\ThisComment####1{}\ProcessComment{#1}}%
\csarg\let{After#1Comment}\TossComment
\CommentEndDef{#1}}
\if 0%
\ifx\fmtname\latexename
0%
\else \ifx\fmtname\latexname
0%
\else
1%
\fi \fi
% latex & latex2e:
\def\EndOfComment#1{\endgroup\end{#1}%
\csname After#1Comment\endcsname}
\def\CommentEndDef#1{{\escapechar=-1\relax
\csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}%
}}
\else
% plain & other
\def\EndOfComment#1{\endgroup\AfterComment}
\def\CommentEndDef#1{{\escapechar=-1\relax
\csarg\xdef{End#1Test}{\string\\end#1}%
}}
\fi
\excludecomment{comment}
\endinput