1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Wed Oct 15 16:06:59 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Wed Oct 15 16:25:31 2008 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  imports Setup
     1.5  begin
     1.6  
     1.7 -setup %invisible {* Code_Target.extend_target ("SML ", ("SML", I)) *}
     1.8 +setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", I)) *}
     1.9  
    1.10  section {* Adaption to target languages \label{sec:adaption} *}
    1.11  
    1.12 @@ -55,13 +55,64 @@
    1.13  subsection {* The adaption principle *}
    1.14  
    1.15  text {*
    1.16 -  \begin{tikzpicture}
    1.17 -    \draw (0, 0) circle (1cm);
    1.18 -    \draw (0.5, 0) circle (0.5cm);
    1.19 -    \draw (0, 0.5) circle (0.5cm);
    1.20 -    \draw (-0.5, 0) circle (0.5cm);
    1.21 -    \draw (0, -0.5) circle (0.5cm);
    1.22 -  \end{tikzpicture}
    1.23 +  The following figure illustrates what \qt{adaption} is conceptually
    1.24 +  supposed to be:
    1.25 +
    1.26 +  \begin{figure}[here]
    1.27 +    \begin{tikzpicture}[scale = 0.5]
    1.28 +      \tikzstyle water=[color = blue, thick]
    1.29 +      \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
    1.30 +      \tikzstyle process=[color = green, semithick, ->]
    1.31 +      \tikzstyle adaption=[color = red, semithick, ->]
    1.32 +      \tikzstyle target=[color = black]
    1.33 +      \foreach \x in {0, ..., 24}
    1.34 +        \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
    1.35 +          + (0.25, -0.25) cos + (0.25, 0.25);
    1.36 +      \draw[style=ice] (1, 0) --
    1.37 +        (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
    1.38 +      \draw[style=ice] (9, 0) --
    1.39 +        (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
    1.40 +      \draw[style=ice] (15, -6) --
    1.41 +        (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
    1.42 +      \draw[style=process]
    1.43 +        (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
    1.44 +      \draw[style=process]
    1.45 +        (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
    1.46 +      \node (adaption) at (11, -2) [style=adaption] {adaption};
    1.47 +      \node at (19, 3) [rotate=90] {generated};
    1.48 +      \node at (19.5, -5) {language};
    1.49 +      \node at (19.5, -3) {library};
    1.50 +      \node (includes) at (19.5, -1) {includes};
    1.51 +      \node (reserved) at (16.5, -3) [rotate=71.57] {reserved};
    1.52 +      \draw[style=process]
    1.53 +        (includes) -- (serialisation);
    1.54 +      \draw[style=process]
    1.55 +        (reserved) -- (serialisation);
    1.56 +      \draw[style=adaption]
    1.57 +        (adaption) -- (serialisation);
    1.58 +      \draw[style=adaption]
    1.59 +        (adaption) -- (includes);
    1.60 +      \draw[style=adaption]
    1.61 +        (adaption) -- (reserved);
    1.62 +    \end{tikzpicture}
    1.63 +    \caption{The adaption principle}
    1.64 +    \label{fig:adaption}
    1.65 +  \end{figure}
    1.66 +
    1.67 +  \noindent In the tame view, code generation acts as broker between
    1.68 +  @{text logic}, @{text "intermediate language"} and
    1.69 +  @{text "target language"} by means of @{text translation} and
    1.70 +  @{text serialisation};  for the latter, the serialiser has to observe
    1.71 +  the structure of the @{text language} itself plus some @{text reserved}
    1.72 +  keywords which have to be avoided for generated code.
    1.73 +  However, if you consider @{text adaption} mechanisms, the code generated
    1.74 +  by the serializer is just the tip of the iceberg:
    1.75 +
    1.76 +  \begin{itemize}
    1.77 +    \item parametrise @{text serialisation}
    1.78 +    \item @{text library} @{text reserved}
    1.79 +    \item @{text "includes"} @{text reserved}
    1.80 +  \end{itemize}
    1.81  *}
    1.82  
    1.83  subsection {* Common adaption cases *}
    1.84 @@ -180,7 +231,7 @@
    1.85    accidental overwrites, using the @{command "code_reserved"} command:
    1.86  *}
    1.87  
    1.88 -code_reserved %quote "SML " bool true false andalso
    1.89 +code_reserved %quote "\<SML>" bool true false andalso
    1.90  
    1.91  text {*
    1.92    \noindent Next, we try to map HOL pairs to SML pairs, using the