# HG changeset patch
# User haftmann
# Date 1285570013 -7200
# Node ID 94b1890e4e4a0be38d7dffb8654bb92e44ba9779
# Parent  793451df8c4ea950fbd84a7da9a9ebc7fa18484b
separate quote tag from tt tag

diff -r 793451df8c4e -r 94b1890e4e4a doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Fri Sep 24 16:09:54 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Mon Sep 27 08:46:53 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)) =
diff -r 793451df8c4e -r 94b1890e4e4a doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Fri Sep 24 16:09:54 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Mon Sep 27 08:46:53 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
diff -r 793451df8c4e -r 94b1890e4e4a doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Fri Sep 24 16:09:54 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Mon Sep 27 08:46:53 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;