src/HOL/IMP/document/isaverbatimwrite.sty
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45246 4fbeabee6487
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     1
\@ifundefined{verbatim@processline}{\input verbatim.sty}{}
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     2
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     3
\newwrite \isaverbatim@out
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     4
\def\openisaverbatimout#1{\immediate\openout \isaverbatim@out #1}
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     5
\def\closeisaverbatimout{\immediate\closeout \isaverbatim@out}
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     6
\def\isaverbatimwrite{%
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     7
  \@bsphack
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     8
  \let\do\@makeother\dospecials
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
     9
  \catcode`\^^M\active \catcode`\^^I=12
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    10
  \def\verbatim@processline{%
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    11
    \immediate\write\isaverbatim@out
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    12
      {\the\verbatim@line}}%
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    13
  \verbatim@start}
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    14
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    15
\def\endisaverbatimwrite{%
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
diff changeset
    16
  \@esphack}