--- a/src/Doc/Codegen/Adaptation.thy Sat Jul 27 21:10:18 2013 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Sat Jul 27 21:21:47 2013 +0200
@@ -71,7 +71,42 @@
conceptually supposed to be:
\begin{figure}[here]
- \includegraphics{adapt}
+ \begin{tikzpicture}[scale = 0.5]
+ \tikzstyle water=[color = blue, thick]
+ \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
+ \tikzstyle process=[color = green, semithick, ->]
+ \tikzstyle adaptation=[color = red, semithick, ->]
+ \tikzstyle target=[color = black]
+ \foreach \x in {0, ..., 24}
+ \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
+ + (0.25, -0.25) cos + (0.25, 0.25);
+ \draw[style=ice] (1, 0) --
+ (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
+ \draw[style=ice] (9, 0) --
+ (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
+ \draw[style=ice] (15, -6) --
+ (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
+ \draw[style=process]
+ (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
+ \draw[style=process]
+ (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
+ \node (adaptation) at (11, -2) [style=adaptation] {adaptation};
+ \node at (19, 3) [rotate=90] {generated};
+ \node at (19.5, -5) {language};
+ \node at (19.5, -3) {library};
+ \node (includes) at (19.5, -1) {includes};
+ \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
+ \draw[style=process]
+ (includes) -- (serialisation);
+ \draw[style=process]
+ (reserved) -- (serialisation);
+ \draw[style=adaptation]
+ (adaptation) -- (serialisation);
+ \draw[style=adaptation]
+ (adaptation) -- (includes);
+ \draw[style=adaptation]
+ (adaptation) -- (reserved);
+ \end{tikzpicture}
\caption{The adaptation principle}
\label{fig:adaptation}
\end{figure}
--- a/src/Doc/Codegen/Foundations.thy Sat Jul 27 21:10:18 2013 +0200
+++ b/src/Doc/Codegen/Foundations.thy Sat Jul 27 21:21:47 2013 +0200
@@ -19,7 +19,37 @@
following picture.
\begin{figure}[h]
- \includegraphics{architecture}
+ \def\sys#1{\emph{#1}}
+ \begin{tikzpicture}[x = 4cm, y = 1cm]
+ \tikzstyle positive=[color = black, fill = white];
+ \tikzstyle negative=[color = white, fill = black];
+ \tikzstyle entity=[rounded corners, draw, thick];
+ \tikzstyle process=[ellipse, draw, thick];
+ \tikzstyle arrow=[-stealth, semithick];
+ \node (spec) at (0, 3) [entity, positive] {specification tools};
+ \node (user) at (1, 3) [entity, positive] {user proofs};
+ \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
+ \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
+ \node (pre) at (1.5, 4) [process, positive] {preprocessing};
+ \node (eqn) at (2.5, 4) [entity, positive] {code equations};
+ \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
+ \node (seri) at (1.5, 0) [process, positive] {serialisation};
+ \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
+ \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
+ \node (Haskell) at (2.5, 1) [entity, positive] {\sys{Haskell}};
+ \node (Scala) at (2.5, 0) [entity, positive] {\sys{Scala}};
+ \draw [semithick] (spec) -- (spec_user_join);
+ \draw [semithick] (user) -- (spec_user_join);
+ \draw [-diamond, semithick] (spec_user_join) -- (raw);
+ \draw [arrow] (raw) -- (pre);
+ \draw [arrow] (pre) -- (eqn);
+ \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
+ \draw [arrow] (iml) -- (seri);
+ \draw [arrow] (seri) -- (SML);
+ \draw [arrow] (seri) -- (OCaml);
+ \draw [arrow] (seri) -- (Haskell);
+ \draw [arrow] (seri) -- (Scala);
+ \end{tikzpicture}
\caption{Code generator architecture}
\label{fig:arch}
\end{figure}
--- a/src/Doc/Codegen/document/adapt.tex Sat Jul 27 21:10:18 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-
-\documentclass[12pt]{article}
-\usepackage{tikz}
-
-\begin{document}
-
-\thispagestyle{empty}
-\setlength{\fboxrule}{0.01pt}
-\setlength{\fboxsep}{4pt}
-
-\fcolorbox{white}{white}{
-
-\begin{tikzpicture}[scale = 0.5]
- \tikzstyle water=[color = blue, thick]
- \tikzstyle ice=[color = black, very thick, cap = round, join = round, fill = white]
- \tikzstyle process=[color = green, semithick, ->]
- \tikzstyle adaptation=[color = red, semithick, ->]
- \tikzstyle target=[color = black]
- \foreach \x in {0, ..., 24}
- \draw[style=water] (\x, 0.25) sin + (0.25, 0.25) cos + (0.25, -0.25) sin
- + (0.25, -0.25) cos + (0.25, 0.25);
- \draw[style=ice] (1, 0) --
- (3, 6) node[above, fill=white] {logic} -- (5, 0) -- cycle;
- \draw[style=ice] (9, 0) --
- (11, 6) node[above, fill=white] {intermediate language} -- (13, 0) -- cycle;
- \draw[style=ice] (15, -6) --
- (19, 6) node[above, fill=white] {target language} -- (23, -6) -- cycle;
- \draw[style=process]
- (3.5, 3) .. controls (7, 5) .. node[fill=white] {translation} (10.5, 3);
- \draw[style=process]
- (11.5, 3) .. controls (15, 5) .. node[fill=white] (serialisation) {serialisation} (18.5, 3);
- \node (adaptation) at (11, -2) [style=adaptation] {adaptation};
- \node at (19, 3) [rotate=90] {generated};
- \node at (19.5, -5) {language};
- \node at (19.5, -3) {library};
- \node (includes) at (19.5, -1) {includes};
- \node (reserved) at (16.5, -3) [rotate=72] {reserved}; % proper 71.57
- \draw[style=process]
- (includes) -- (serialisation);
- \draw[style=process]
- (reserved) -- (serialisation);
- \draw[style=adaptation]
- (adaptation) -- (serialisation);
- \draw[style=adaptation]
- (adaptation) -- (includes);
- \draw[style=adaptation]
- (adaptation) -- (reserved);
-\end{tikzpicture}
-
-}
-
-\end{document}
--- a/src/Doc/Codegen/document/architecture.tex Sat Jul 27 21:10:18 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-
-\documentclass[12pt]{article}
-\usepackage{tikz}
-\usetikzlibrary{shapes}
-\usetikzlibrary{arrows}
-
-\begin{document}
-
-\thispagestyle{empty}
-\setlength{\fboxrule}{0.01pt}
-\setlength{\fboxsep}{4pt}
-
-\fcolorbox{white}{white}{
-
-\newcommand{\sys}[1]{\emph{#1}}
-
-\begin{tikzpicture}[x = 4cm, y = 1cm]
- \tikzstyle positive=[color = black, fill = white];
- \tikzstyle negative=[color = white, fill = black];
- \tikzstyle entity=[rounded corners, draw, thick];
- \tikzstyle process=[ellipse, draw, thick];
- \tikzstyle arrow=[-stealth, semithick];
- \node (spec) at (0, 3) [entity, positive] {specification tools};
- \node (user) at (1, 3) [entity, positive] {user proofs};
- \node (spec_user_join) at (0.5, 3) [shape=coordinate] {};
- \node (raw) at (0.5, 4) [entity, positive] {raw code equations};
- \node (pre) at (1.5, 4) [process, positive] {preprocessing};
- \node (eqn) at (2.5, 4) [entity, positive] {code equations};
- \node (iml) at (0.5, 0) [entity, positive] {intermediate program};
- \node (seri) at (1.5, 0) [process, positive] {serialisation};
- \node (SML) at (2.5, 3) [entity, positive] {\sys{SML}};
- \node (OCaml) at (2.5, 2) [entity, positive] {\sys{OCaml}};
- \node (Haskell) at (2.5, 1) [entity, positive] {\sys{Haskell}};
- \node (Scala) at (2.5, 0) [entity, positive] {\sys{Scala}};
- \draw [semithick] (spec) -- (spec_user_join);
- \draw [semithick] (user) -- (spec_user_join);
- \draw [-diamond, semithick] (spec_user_join) -- (raw);
- \draw [arrow] (raw) -- (pre);
- \draw [arrow] (pre) -- (eqn);
- \draw [arrow] (eqn) -- node (transl) [process, positive] {translation} (iml);
- \draw [arrow] (iml) -- (seri);
- \draw [arrow] (seri) -- (SML);
- \draw [arrow] (seri) -- (OCaml);
- \draw [arrow] (seri) -- (Haskell);
- \draw [arrow] (seri) -- (Scala);
-\end{tikzpicture}
-
-}
-
-\end{document}
--- a/src/Doc/Codegen/document/build Sat Jul 27 21:10:18 2013 +0200
+++ b/src/Doc/Codegen/document/build Sat Jul 27 21:21:47 2013 +0200
@@ -12,12 +12,5 @@
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
-for NAME in architecture adapt
-do
- latex "$NAME"
- $ISABELLE_DVIPS -E -o "$NAME.eps" "$NAME.dvi"
- $ISABELLE_EPSTOPDF "$NAME.eps"
-done
-
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
--- a/src/Doc/Codegen/document/root.tex Sat Jul 27 21:10:18 2013 +0200
+++ b/src/Doc/Codegen/document/root.tex Sat Jul 27 21:21:47 2013 +0200
@@ -1,6 +1,7 @@
\documentclass[12pt,a4paper,fleqn]{article}
\usepackage{latexsym,graphicx}
+\usepackage{tikz}\usetikzlibrary{shapes}\usetikzlibrary{arrows}
\usepackage{multirow}
\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
--- a/src/Doc/ROOT Sat Jul 27 21:10:18 2013 +0200
+++ b/src/Doc/ROOT Sat Jul 27 21:21:47 2013 +0200
@@ -33,8 +33,6 @@
"../extra.sty"
"../isar.sty"
"../manual.bib"
- "document/adapt.tex"
- "document/architecture.tex"
"document/build"
"document/root.tex"
"document/style.sty"