# HG changeset patch # User haftmann # Date 1285337394 -7200 # Node ID 793451df8c4ea950fbd84a7da9a9ebc7fa18484b # Parent e75b993c04334598330b7f460c77669820cf29ab separate quote tag from tt tag diff -r e75b993c0433 -r 793451df8c4e doc-src/Codegen/Thy/Adaptation.thy --- a/doc-src/Codegen/Thy/Adaptation.thy Fri Sep 24 15:53:57 2010 +0200 +++ b/doc-src/Codegen/Thy/Adaptation.thy Fri Sep 24 16:09:54 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 \" +code_const %quote %tt True and False and "op \" (SML "true" and "false" and "_ andalso _") text {* @@ -218,7 +218,7 @@ precedences which may be used here: *} -code_const %quotett "op \" +code_const %quote %tt "op \" (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 diff -r e75b993c0433 -r 793451df8c4e doc-src/Codegen/style.sty --- a/doc-src/Codegen/style.sty Fri Sep 24 15:53:57 2010 +0200 +++ b/doc-src/Codegen/style.sty Fri Sep 24 16:09:54 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}