src/HOL/HOLCF/IMP/document/isaverbatimwrite.sty
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 45277 85b0ca9dd82f
permissions -rw-r--r--
proper syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45277
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     1
\@ifundefined{verbatim@processline}{\input verbatim.sty}{}
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     2
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     3
\newwrite \isaverbatim@out
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     4
\def\openisaverbatimout#1{\immediate\openout \isaverbatim@out #1}
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     5
\def\closeisaverbatimout{\immediate\closeout \isaverbatim@out}
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     6
\def\isaverbatimwrite{%
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     7
  \@bsphack
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     8
  \let\do\@makeother\dospecials
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
     9
  \catcode`\^^M\active \catcode`\^^I=12
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    10
  \def\verbatim@processline{%
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    11
    \immediate\write\isaverbatim@out
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    12
      {\the\verbatim@line}}%
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    13
  \verbatim@start}
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    14
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    15
\def\endisaverbatimwrite{%
85b0ca9dd82f uses IMP and hence requires its tex setup
nipkow
parents:
diff changeset
    16
  \@esphack}