--- a/doc-src/Codegen/Thy/Adaptation.thy Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy Mon Sep 27 08:47:23 2010 +0200
@@ -190,9 +190,9 @@
"bool"}, we may use \qn{custom serialisations}:
*}
-code_type %quotett bool
+code_type %quote %tt bool
(SML "bool")
-code_const %quotett True and False and "op \<and>"
+code_const %quote %tt True and False and "op \<and>"
(SML "true" and "false" and "_ andalso _")
text {*
@@ -218,7 +218,7 @@
precedences which may be used here:
*}
-code_const %quotett "op \<and>"
+code_const %quote %tt "op \<and>"
(SML infixl 1 "andalso")
text %quote %typewriter {*
@@ -247,9 +247,9 @@
code_const %invisible Pair
(SML)
(*>*)
-code_type %quotett prod
+code_type %quote %tt prod
(SML infix 2 "*")
-code_const %quotett Pair
+code_const %quote %tt Pair
(SML "!((_),/ (_))")
text {*
@@ -283,10 +283,10 @@
@{command_def code_class}) and its operation @{const [source] HOL.equal}
*}
-code_class %quotett equal
+code_class %quote %tt equal
(Haskell "Eq")
-code_const %quotett "HOL.equal"
+code_const %quote %tt "HOL.equal"
(Haskell infixl 4 "==")
text {*
@@ -307,7 +307,7 @@
end %quote (*<*)
-(*>*) code_type %quotett bar
+(*>*) code_type %quote %tt bar
(Haskell "Integer")
text {*
@@ -316,7 +316,7 @@
suppress this additional instance, use @{command_def "code_instance"}:
*}
-code_instance %quotett bar :: equal
+code_instance %quote %tt bar :: equal
(Haskell -)
@@ -328,10 +328,10 @@
"code_include"} command:
*}
-code_include %quotett Haskell "Errno"
+code_include %quote %tt Haskell "Errno"
{*errno i = error ("Error number: " ++ show i)*}
-code_reserved %quotett Haskell Errno
+code_reserved %quote %tt Haskell Errno
text {*
\noindent Such named @{text include}s are then prepended to every
--- a/doc-src/Codegen/Thy/Evaluation.thy Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy Mon Sep 27 08:47:23 2010 +0200
@@ -206,7 +206,7 @@
datatype %quote form = T | F | And form form | Or form form (*<*)
-(*>*) ML %quotett {*
+(*>*) ML %tt %quote {*
fun eval_form @{code T} = true
| eval_form @{code F} = false
| eval_form (@{code And} (p, q)) =
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Mon Sep 27 08:47:23 2010 +0200
@@ -281,23 +281,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\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}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\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
@@ -354,20 +354,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}const}\isamarkupfalse%
\ {\isachardoublequoteopen}op\ {\isasymand}{\isachardoublequoteclose}\isanewline
\ \ {\isacharparenleft}SML\ \isakeyword{infixl}\ {\isadigit{1}}\ {\isachardoublequoteopen}andalso{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\isadelimtypewriter
%
@@ -447,23 +447,23 @@
%
\endisadeliminvisible
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\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}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent The initial bang ``\verb|!|'' tells the serialiser
@@ -499,11 +499,11 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\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}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent A problem now occurs whenever a type which is an instance
@@ -553,20 +553,20 @@
%
\endisadelimquote
%
-\isadelimquotett
+\isadelimtt
\ %
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}type}\isamarkupfalse%
\ bar\isanewline
\ \ {\isacharparenleft}Haskell\ {\isachardoublequoteopen}Integer{\isachardoublequoteclose}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent The code generator would produce an additional instance,
@@ -575,20 +575,20 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\isacommand{code{\isacharunderscore}instance}\isamarkupfalse%
\ bar\ {\isacharcolon}{\isacharcolon}\ equal\isanewline
\ \ {\isacharparenleft}Haskell\ {\isacharminus}{\isacharparenright}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
}
@@ -600,23 +600,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
-\isatagquotett
+\isatagtt
\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%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagtt
+{\isafoldtt}%
%
-\isadelimquotett
+\isadelimtt
%
-\endisadelimquotett
+\endisadelimtt
%
\begin{isamarkuptext}%
\noindent Such named \isa{include}s are then prepended to every
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Mon Sep 27 08:47:23 2010 +0200
@@ -269,20 +269,7 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ %
-\endisatagquote
-{\isafoldquote}%
-%
-\isadelimquote
-%
-\endisadelimquote
-%
-\isadelimquotett
-\ %
-\endisadelimquotett
-%
-\isatagquotett
-\isacommand{ML}\isamarkupfalse%
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\ \ \isacommand{ML}\isamarkupfalse%
\ {\isacharverbatimopen}\isanewline
\ \ fun\ eval{\isacharunderscore}form\ %
\isaantiq
@@ -307,12 +294,12 @@
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
-\endisatagquotett
-{\isafoldquotett}%
+\endisatagquote
+{\isafoldquote}%
%
-\isadelimquotett
+\isadelimquote
%
-\endisadelimquotett
+\endisadelimquote
%
\begin{isamarkuptext}%
\noindent \isa{code} takes as argument the name of a constant;
--- a/doc-src/Codegen/style.sty Sat Sep 25 10:32:14 2010 +0200
+++ b/doc-src/Codegen/style.sty Mon Sep 27 08:47:23 2010 +0200
@@ -37,9 +37,8 @@
\renewcommand{\isatagtypewriter}{\begin{typewriter}}
\renewcommand{\endisatagtypewriter}{\end{typewriter}}
-\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quote}}
+\isakeeptag{tt}
+\renewcommand{\isatagtt}{\isabellestyle{tt}\isastyle}
%% a trick
\newcommand{\isasymSML}{SML}