src/HOL/HOLCF/IMP/document/isaverbatimwrite.sty
author haftmann
Sun, 27 Jul 2025 17:52:06 +0200
changeset 82909 e4fae2227594
parent 45277 85b0ca9dd82f
permissions -rw-r--r--
added missing colon
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}