Re: [isabelle] Unable to get document preparation system to work



On Wed, 29 Jan 2014, Makarius wrote:

On Wed, 29 Jan 2014, James Lingard wrote:

>    comment.sty   9666    2014-01-23 07:36:21
>
 That's weird.  The copyright at the top of the file says July 2009.  If it
 really is brand new then that explains why I might have been the first
 person to run into this.

So from where did you get that version?  TeXlive is not there yet, luckily.

I use myself CTAN only as occasional reference, but have no idea how it is actually maintained. There is also no immediately visible changeset history, with names of authors etc.

Maybe it is just an accident, with some experiment that someone made at some point, to the anoyance of plain TeX users.

I've looked again more closely at CTAN: the situation of http://www.ctan.org/tex-archive/macros/latex2e/contrib/comment is a bit odd, because comment.sty has been copied over with that 3.7 version from 2009, while everything else is still saying 3.6, including the documentation (which claims that the package works with Plain TeX).

I've also tried again if it is feasible to run in regular LaTeX mode, but then it is very slow, as already noticed in 2005, when I made this setup for isabelle.sty.


So the present conclusion of this thread: Anybody who happens to be on a latest-testing-unstable branch of some TeX installation can put a copy of the included comment.sty 3.6 into $ISABELLE_HOME/lib/texinputs/. The Isabelle document preparation system will copy it from there into the document output directory, so that version should take precedence.

The next Isabelle release will probably have that comment.sty 3.6 as well, but that is still several months ahead.


	Makarius
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 at 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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.