# HG changeset patch # User haftmann # Date 1285597176 -7200 # Node ID 7aef0e4a3aac442a00eb19681a357ef2ce153f8b # Parent 832c42be723e09933bc884376c0bf73bc601eede combine quote and typewriter tag diff -r 832c42be723e -r 7aef0e4a3aac doc-src/Classes/Thy/Classes.thy --- a/doc-src/Classes/Thy/Classes.thy Mon Sep 27 14:13:22 2010 +0200 +++ b/doc-src/Classes/Thy/Classes.thy Mon Sep 27 16:19:36 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)} *} diff -r 832c42be723e -r 7aef0e4a3aac doc-src/Classes/Thy/document/Classes.tex --- a/doc-src/Classes/Thy/document/Classes.tex Mon Sep 27 14:13:22 2010 +0200 +++ b/doc-src/Classes/Thy/document/Classes.tex Mon Sep 27 16:19:36 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% }