doc-src/IsarAdvanced/Codegen/Thy/document/Adaption.tex

   keywords which have to be avoided for generated code.
   However, if you consider \isa{adaption} mechanisms, the code generated
   by the serializer is just the tip of the iceberg:
 
   \begin{itemize}
-    \item parametrise \isa{serialisation}
-    \item \isa{library} \isa{reserved}
-    \item \isa{includes} \isa{reserved}
-  \end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Common adaption cases%
+    \item \isa{serialisation} can be \emph{parametrised} such that
+      logical entities are mapped to target-specific ones
+      (e.g. target-specific list syntax,
+        see also \secref{sec:adaption_mechanisms})
+    \item Such parametrisations can involve references to a
+      target-specific standard \isa{library} (e.g. using
+      the \isa{Haskell} \verb|Maybe| type instead
+      of the \isa{HOL} \isa{option} type);
+      if such are used, the corresponding identifiers
+      (in our example, \verb|Maybe|, \verb|Nothing|
+      and \verb|Just|) also have to be considered \isa{reserved}.
+    \item Even more, the user can enrich the library of the
+      target-language by providing code snippets
+      (\qt{\isa{includes}}) which are prepended to
+      any generated code (see \secref{sec:include});  this typically
+      also involves further \isa{reserved} identifiers.
+  \end{itemize}
+
+  \noindent As figure \ref{fig:adaption} illustrates, all these adaption mechanisms
+  have to act consistently;  it is at the discretion of the user
+  to take care for this.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Common adaption patterns%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code

     strange effects may occur otherwise.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Adaption mechanisms \label{sec:adaption_mechanisms}%
+\isamarkupsubsection{Parametrising serialisation \label{sec:adaption_mechanisms}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 Consider the following function and its corresponding

 %
 \isadelimquotett
 %
 \endisadelimquotett
 %
-\isamarkupsubsection{Enhancing the target language context%
+\isamarkupsubsection{Enhancing the target language context \label{sec:include}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 In rare cases it is necessary to \emph{enrich} the context of a