# HG changeset patch
# User haftmann
# Date 1285332976 -7200
# Node ID a0d49ed5a23a3ad5f550b6cd67723d34d23a2402
# Parent  d36864e3f06c4881ec2b4204a4a34f9f91cc54b2
use typewriter tag instead of bare environment

diff -r d36864e3f06c -r a0d49ed5a23a doc-src/Classes/Thy/Classes.thy
--- a/doc-src/Classes/Thy/Classes.thy	Fri Sep 24 14:03:44 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Fri Sep 24 14:56:16 2010 +0200
@@ -601,19 +601,15 @@
   \noindent This maps to Haskell as follows:
 *}
 (*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts example (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts example (Haskell)}
 *}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts example (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts example (SML)}
 *}
 
 
@@ -621,10 +617,8 @@
   \noindent In Scala, implicts are used as dictionaries:
 *}
 (*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts example (Scala)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts example (Scala)}
 *}
 
 
diff -r d36864e3f06c -r a0d49ed5a23a doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Fri Sep 24 14:03:44 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex	Fri Sep 24 14:56:16 2010 +0200
@@ -1123,15 +1123,14 @@
 %
 \endisadeliminvisible
 %
-\isadelimquote
+\isadelimtypewriter
 %
-\endisadelimquote
+\endisadelimtypewriter
 %
-\isatagquote
+\isatagtypewriter
 %
 \begin{isamarkuptext}%
-\begin{typewriter}
-    module\ Example\ where\ {\isacharbraceleft}\isanewline
+module\ Example\ where\ {\isacharbraceleft}\isanewline
 \isanewline
 data\ Nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ Nat{\isacharsemicolon}\isanewline
 \isanewline
@@ -1192,33 +1191,30 @@
 example\ {\isacharcolon}{\isacharcolon}\ Integer{\isacharsemicolon}\isanewline
 example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
 \isanewline
-{\isacharbraceright}\isanewline
-
-  \end{typewriter}%
+{\isacharbraceright}\isanewline%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
 %
-\isadelimquote
+\isadelimtypewriter
 %
-\endisadelimquote
+\endisadelimtypewriter
 %
 \begin{isamarkuptext}%
 \noindent The code in SML has explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimquote
+\isadelimtypewriter
 %
-\endisadelimquote
+\endisadelimtypewriter
 %
-\isatagquote
+\isatagtypewriter
 %
 \begin{isamarkuptext}%
-\begin{typewriter}
-    structure\ Example\ {\isacharcolon}\ sig\isanewline
+structure\ Example\ {\isacharcolon}\ sig\isanewline
 \ \ datatype\ nat\ {\isacharequal}\ Zero{\isacharunderscore}nat\ {\isacharbar}\ Suc\ of\ nat\isanewline
 \ \ val\ nat{\isacharunderscore}aux\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\ {\isacharminus}{\isachargreater}\ nat\isanewline
 \ \ val\ nat\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharminus}{\isachargreater}\ nat\isanewline
@@ -1295,18 +1291,16 @@
 val\ example\ {\isacharcolon}\ IntInf{\isachardot}int\ {\isacharequal}\isanewline
 \ \ pow{\isacharunderscore}int\ group{\isacharunderscore}int\ {\isacharparenleft}{\isadigit{1}}{\isadigit{0}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}\ {\isacharparenleft}{\isachartilde}{\isadigit{2}}\ {\isacharcolon}\ IntInf{\isachardot}int{\isacharparenright}{\isacharsemicolon}\isanewline
 \isanewline
-end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline
-
-  \end{typewriter}%
+end{\isacharsemicolon}\ {\isacharparenleft}{\isacharasterisk}struct\ Example{\isacharasterisk}{\isacharparenright}\isanewline%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
 %
-\isadelimquote
+\isadelimtypewriter
 %
-\endisadelimquote
+\endisadelimtypewriter
 %
 \begin{isamarkuptext}%
 \noindent In Scala, implicts are used as dictionaries:%
@@ -1326,15 +1320,14 @@
 %
 \endisadeliminvisible
 %
-\isadelimquote
+\isadelimtypewriter
 %
-\endisadelimquote
+\endisadelimtypewriter
 %
-\isatagquote
+\isatagtypewriter
 %
 \begin{isamarkuptext}%
-\begin{typewriter}
-    object\ Example\ {\isacharbraceleft}\isanewline
+object\ Example\ {\isacharbraceleft}\isanewline
 \isanewline
 abstract\ sealed\ class\ nat\isanewline
 final\ case\ object\ Zero{\isacharunderscore}nat\ extends\ nat\isanewline
@@ -1401,18 +1394,16 @@
 \isanewline
 def\ example{\isacharcolon}\ BigInt\ {\isacharequal}\ pow{\isacharunderscore}int{\isacharbrackleft}BigInt{\isacharbrackright}{\isacharparenleft}BigInt{\isacharparenleft}{\isadigit{1}}{\isadigit{0}}{\isacharparenright}{\isacharcomma}\ BigInt{\isacharparenleft}{\isacharminus}\ {\isadigit{2}}{\isacharparenright}{\isacharparenright}\isanewline
 \isanewline
-{\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline
-
-  \end{typewriter}%
+{\isacharbraceright}\ {\isacharslash}{\isacharasterisk}\ object\ Example\ {\isacharasterisk}{\isacharslash}\isanewline%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagquote
-{\isafoldquote}%
+\endisatagtypewriter
+{\isafoldtypewriter}%
 %
-\isadelimquote
+\isadelimtypewriter
 %
-\endisadelimquote
+\endisadelimtypewriter
 %
 \isamarkupsubsection{Inspecting the type class universe%
 }
diff -r d36864e3f06c -r a0d49ed5a23a doc-src/Classes/style.sty
--- a/doc-src/Classes/style.sty	Fri Sep 24 14:03:44 2010 +0200
+++ b/doc-src/Classes/style.sty	Fri Sep 24 14:56:16 2010 +0200
@@ -28,10 +28,14 @@
 \newcommand{\quotebreak}{\\[1.2ex]}
 
 %% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}%
+\isakeeptag{typewriter}
+\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
+\renewcommand{\isadigit}[1]{{##1}}%
 \parindent0pt%
 \isabellestyle{tt}\isastyle%
 \fontsize{9pt}{9pt}\selectfont}{}
+\renewcommand{\isatagtypewriter}{\begin{typewriter}}
+\renewcommand{\endisatagtypewriter}{\end{typewriter}}
 
 %% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
diff -r d36864e3f06c -r a0d49ed5a23a doc-src/Codegen/style.sty
--- a/doc-src/Codegen/style.sty	Fri Sep 24 14:03:44 2010 +0200
+++ b/doc-src/Codegen/style.sty	Fri Sep 24 14:56:16 2010 +0200
@@ -28,10 +28,14 @@
 \newcommand{\quotebreak}{\\[1.2ex]}
 
 %% typewriter text
-\newenvironment{typewriter}{\renewcommand{\isadigit}[1]{{##1}}%
+\isakeeptag{typewriter}
+\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
+\renewcommand{\isadigit}[1]{{##1}}%
 \parindent0pt%
 \isabellestyle{tt}\isastyle%
 \fontsize{9pt}{9pt}\selectfont}{}
+\renewcommand{\isatagtypewriter}{\begin{typewriter}}
+\renewcommand{\endisatagtypewriter}{\end{typewriter}}
 
 \isakeeptag{quotett}
 \renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}