--- a/doc-src/Classes/Thy/Classes.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Mon Sep 27 16:32:48 2010 +0200
@@ -601,14 +601,14 @@
\noindent This maps to Haskell as follows:
*}
(*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (Haskell)}
*}
text {*
\noindent The code in SML has explicit dictionary passing:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (SML)}
*}
@@ -617,7 +617,7 @@
\noindent In Scala, implicts are used as dictionaries:
*}
(*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (Scala)}
*}
--- a/doc-src/Classes/Thy/document/Classes.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Mon Sep 27 16:32:48 2010 +0200
@@ -1123,11 +1123,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -1195,23 +1195,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -1295,12 +1295,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent In Scala, implicts are used as dictionaries:%
@@ -1320,11 +1320,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
object\ Example\ {\isacharbraceleft}\isanewline
@@ -1398,12 +1398,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Inspecting the type class universe%
}
--- a/doc-src/Classes/style.sty Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Classes/style.sty Mon Sep 27 16:32:48 2010 +0200
@@ -28,14 +28,16 @@
\newcommand{\quotebreak}{\\[1.2ex]}
%% typewriter text
-\isakeeptag{typewriter}
\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
\renewcommand{\isadigit}[1]{{##1}}%
\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
\isabellestyle{tt}\isastyle%
\fontsize{9pt}{9pt}\selectfont}{}
-\renewcommand{\isatagtypewriter}{\begin{typewriter}}
-\renewcommand{\endisatagtypewriter}{\end{typewriter}}
+
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
--- a/doc-src/Codegen/Thy/Adaptation.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Mon Sep 27 16:32:48 2010 +0200
@@ -175,7 +175,7 @@
code_const %invisible True and False and "op \<and>" and Not
(SML and and and)
(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts in_interval (SML)}
*}
@@ -190,9 +190,9 @@
"bool"}, we may use \qn{custom serialisations}:
*}
-code_type %quote %tt bool
+code_type %quotett bool
(SML "bool")
-code_const %quote %tt True and False and "op \<and>"
+code_const %quotett True and False and "op \<and>"
(SML "true" and "false" and "_ andalso _")
text {*
@@ -206,7 +206,7 @@
placeholder for the type constructor's (the constant's) arguments.
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts in_interval (SML)}
*}
@@ -218,10 +218,10 @@
precedences which may be used here:
*}
-code_const %quote %tt "op \<and>"
+code_const %quotett "op \<and>"
(SML infixl 1 "andalso")
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts in_interval (SML)}
*}
@@ -247,9 +247,9 @@
code_const %invisible Pair
(SML)
(*>*)
-code_type %quote %tt prod
+code_type %quotett prod
(SML infix 2 "*")
-code_const %quote %tt Pair
+code_const %quotett Pair
(SML "!((_),/ (_))")
text {*
@@ -283,10 +283,10 @@
@{command_def code_class}) and its operation @{const [source] HOL.equal}
*}
-code_class %quote %tt equal
+code_class %quotett equal
(Haskell "Eq")
-code_const %quote %tt "HOL.equal"
+code_const %quotett "HOL.equal"
(Haskell infixl 4 "==")
text {*
@@ -307,7 +307,7 @@
end %quote (*<*)
-(*>*) code_type %quote %tt bar
+(*>*) code_type %quotett bar
(Haskell "Integer")
text {*
@@ -316,7 +316,7 @@
suppress this additional instance, use @{command_def "code_instance"}:
*}
-code_instance %quote %tt bar :: equal
+code_instance %quotett bar :: equal
(Haskell -)
@@ -328,10 +328,10 @@
"code_include"} command:
*}
-code_include %quote %tt Haskell "Errno"
+code_include %quotett Haskell "Errno"
{*errno i = error ("Error number: " ++ show i)*}
-code_reserved %quote %tt Haskell Errno
+code_reserved %quotett Haskell Errno
text {*
\noindent Such named @{text include}s are then prepended to every
--- a/doc-src/Codegen/Thy/Evaluation.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Mon Sep 27 16:32:48 2010 +0200
@@ -206,7 +206,7 @@
datatype %quote form = T | F | And form form | Or form form (*<*)
-(*>*) ML %tt %quote {*
+(*>*) ML %quotett {*
fun eval_form @{code T} = true
| eval_form @{code F} = false
| eval_form (@{code And} (p, q)) =
--- a/doc-src/Codegen/Thy/Foundations.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/Foundations.thy Mon Sep 27 16:32:48 2010 +0200
@@ -161,7 +161,7 @@
is determined syntactically. The resulting code:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts dequeue (consts) dequeue (Haskell)}
*}
@@ -217,7 +217,7 @@
equality check, as can be seen in the corresponding @{text SML} code:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts collect_duplicates (SML)}
*}
@@ -255,7 +255,7 @@
for the pattern @{term "AQueue [] []"}:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
*}
@@ -296,7 +296,7 @@
exception at the appropriate position:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
*}
--- a/doc-src/Codegen/Thy/Further.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy Mon Sep 27 16:32:48 2010 +0200
@@ -112,7 +112,7 @@
After this setup procedure, code generation can continue as usual:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts funpows (consts) Nat.funpow funpows (Haskell)}
*}
--- a/doc-src/Codegen/Thy/Introduction.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/Introduction.thy Mon Sep 27 16:32:48 2010 +0200
@@ -70,7 +70,7 @@
text {* \noindent resulting in the following code: *}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts empty enqueue dequeue (SML)}
*}
@@ -93,7 +93,7 @@
\noindent This is the corresponding code:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts empty enqueue dequeue (Haskell)}
*}
@@ -168,7 +168,7 @@
native classes:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts bexp (Haskell)}
*}
@@ -178,7 +178,7 @@
@{text SML}:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts bexp (SML)}
*}
--- a/doc-src/Codegen/Thy/Refinement.thy Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/Refinement.thy Mon Sep 27 16:32:48 2010 +0200
@@ -31,7 +31,7 @@
to two recursive calls:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts fib (consts) fib (Haskell)}
*}
@@ -69,7 +69,7 @@
\noindent The resulting code shows only linear growth of runtime:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts fib (consts) fib fib_step (Haskell)}
*}
@@ -157,7 +157,7 @@
\noindent The resulting code looks as expected:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts empty enqueue dequeue (SML)}
*}
@@ -253,7 +253,7 @@
\noindent Then the corresponding code is as follows:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
*} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Mon Sep 27 16:32:48 2010 +0200
@@ -228,11 +228,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -264,12 +264,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Though this is correct code, it is a little bit
@@ -281,23 +281,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bool\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}bool{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ True\ \isakeyword{and}\ False\ \isakeyword{and}\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}true{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}false{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}{\isacharunderscore}\ andalso\ {\isacharunderscore}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{code\_type}\hypertarget{command.code-type}{\hyperlink{command.code-type}{\mbox{\isa{\isacommand{code{\isacharunderscore}type}}}}} command takes a type constructor
@@ -311,11 +311,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -338,12 +338,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This still is not perfect: the parentheses around the
@@ -354,26 +354,26 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -396,12 +396,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The attentive reader may ask how we assert that no
@@ -447,23 +447,23 @@
%
\endisadeliminvisible
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ prod\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infix}\ {\isadigit{2}}\ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}{\isacharparenright}\isanewline
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ Pair\isanewline
\ \ {\isacharparenleft}SML\ {\isachardoublequoteopen}{\isacharbang}{\isacharparenleft}{\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharcomma}{\isacharslash}\ {\isacharparenleft}{\isacharunderscore}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The initial bang ``\verb|!|'' tells the serialiser
@@ -499,11 +499,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}class}\isamarkupfalse%
\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Eq{\isachardoublequoteclose}{\isacharparenright}\isanewline
@@ -511,12 +511,12 @@
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}HOL{\isachardot}equal{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}Haskell\ \isakeyword{infixl}\ {\isadigit{4}}\ {\isachardoublequoteopen}{\isacharequal}{\isacharequal}{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent A problem now occurs whenever a type which is an instance
@@ -553,20 +553,20 @@
%
\endisadelimquote
%
-\isadelimtt
+\isadelimquotett
\ %
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bar\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent The code generator would produce an additional instance,
@@ -575,20 +575,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
\ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
}
@@ -600,23 +600,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
-\isatagtt
+\isatagquotett
\isacommand{code{\isacharunderscore}include}\isamarkupfalse%
\ Haskell\ {\isachardoublequoteopen}Errno{\isachardoublequoteclose}\isanewline
{\isacharverbatimopen}errno\ i\ {\isacharequal}\ error\ {\isacharparenleft}{\isachardoublequote}Error\ number{\isacharcolon}\ {\isachardoublequote}\ {\isacharplus}{\isacharplus}\ show\ i{\isacharparenright}{\isacharverbatimclose}\isanewline
\isanewline
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
\ Haskell\ Errno%
-\endisatagtt
-{\isafoldtt}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimtt
+\isadelimquotett
%
-\endisadelimtt
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent Such named \isa{include}s are then prepended to every
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 16:32:48 2010 +0200
@@ -269,7 +269,20 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isadelimquotett
+\ %
+\endisadelimquotett
+%
+\isatagquotett
+\isacommand{ML}\isamarkupfalse%
\ {\isacharverbatimopen}\isanewline
\ \ fun\ eval{\isacharunderscore}form\ %
\isaantiq
@@ -294,12 +307,12 @@
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimquote
+\isadelimquotett
%
-\endisadelimquote
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent \isa{code} takes as argument the name of a constant;
--- a/doc-src/Codegen/Thy/document/Foundations.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Foundations.tex Mon Sep 27 16:32:48 2010 +0200
@@ -238,11 +238,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Maybe\ a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -253,12 +253,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has
@@ -338,11 +338,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -373,12 +373,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Obviously, polymorphic equality is implemented the Haskell
@@ -431,11 +431,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Queue\ a\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a{\isacharcomma}\ Queue\ a{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -447,12 +447,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent In some cases it is desirable to have this
@@ -520,11 +520,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ a{\isacharsemicolon}\isanewline
@@ -538,12 +538,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This feature however is rarely needed in practice. Note
--- a/doc-src/Codegen/Thy/document/Further.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Further.tex Mon Sep 27 16:32:48 2010 +0200
@@ -207,11 +207,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
funpow\ {\isacharcolon}{\isacharcolon}\ forall\ a{\isachardot}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}a\ {\isacharminus}{\isachargreater}\ a{\isacharparenright}\ {\isacharminus}{\isachargreater}\ a\ {\isacharminus}{\isachargreater}\ a{\isacharsemicolon}\isanewline
@@ -224,12 +224,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Imperative data structures%
}
--- a/doc-src/Codegen/Thy/document/Introduction.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Sep 27 16:32:48 2010 +0200
@@ -133,11 +133,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -176,12 +176,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The \indexdef{}{command}{export\_code}\hypertarget{command.export-code}{\hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}}} command takes a
@@ -216,11 +216,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -245,12 +245,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent For more details about \hyperlink{command.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} see
@@ -382,11 +382,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -431,12 +431,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent This is a convenient place to show how explicit dictionary
@@ -445,11 +445,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -499,12 +499,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent Note the parameters with trailing underscore (\verb|A_|), which are the dictionary parameters.%
--- a/doc-src/Codegen/Thy/document/Refinement.tex Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Mon Sep 27 16:32:48 2010 +0200
@@ -65,11 +65,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
fib\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ Nat{\isacharsemicolon}\isanewline
@@ -79,12 +79,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent A more efficient implementation would use dynamic
@@ -161,11 +161,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
fib{\isacharunderscore}step\ {\isacharcolon}{\isacharcolon}\ Nat\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}Nat{\isacharcomma}\ Nat{\isacharparenright}{\isacharsemicolon}\isanewline
@@ -180,12 +180,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Datatype refinement%
}
@@ -337,11 +337,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -380,12 +380,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
The same techniques can also be applied to types which are not
@@ -571,11 +571,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -609,12 +609,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
Typical data structures implemented by representations involving
--- a/doc-src/Codegen/style.sty Mon Sep 27 14:54:10 2010 +0200
+++ b/doc-src/Codegen/style.sty Mon Sep 27 16:32:48 2010 +0200
@@ -28,17 +28,20 @@
\newcommand{\quotebreak}{\\[1.2ex]}
%% typewriter text
-\isakeeptag{typewriter}
\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
\renewcommand{\isadigit}[1]{{##1}}%
\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
\isabellestyle{tt}\isastyle%
\fontsize{9pt}{9pt}\selectfont}{}
-\renewcommand{\isatagtypewriter}{\begin{typewriter}}
-\renewcommand{\endisatagtypewriter}{\end{typewriter}}
-\isakeeptag{tt}
-\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
+
+\isakeeptag{quotett}
+\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quote}}
%% a trick
\newcommand{\isasymSML}{SML}