src/HOL/HOLCF/IMP/document/isaverbatimwrite.sty
author wenzelm
Wed, 11 Oct 2017 21:41:11 +0200
changeset 66846 c04f46a6f29d
parent 45277 85b0ca9dd82f
permissions -rw-r--r--
back to build_polyml_component according to 54c6ec4166a4 (amending 808e6ddb5a50);

\@ifundefined{verbatim@processline}{\input verbatim.sty}{}

\newwrite \isaverbatim@out
\def\openisaverbatimout#1{\immediate\openout \isaverbatim@out #1}
\def\closeisaverbatimout{\immediate\closeout \isaverbatim@out}
\def\isaverbatimwrite{%
  \@bsphack
  \let\do\@makeother\dospecials
  \catcode`\^^M\active \catcode`\^^I=12
  \def\verbatim@processline{%
    \immediate\write\isaverbatim@out
      {\the\verbatim@line}}%
  \verbatim@start}

\def\endisaverbatimwrite{%
  \@esphack}