# HG changeset patch # User wenzelm # Date 1374952907 -7200 # Node ID e7296939fec2e12b4b6c77b51595d89057ea5fc4 # Parent c08bd0a219f88f6dd353b6a1ade93d71bedc7e31 more direct inclusion of tikz pictures; diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/Codegen/Adaptation.thy --- 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} diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/Codegen/Foundations.thy --- 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} diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/Codegen/document/adapt.tex --- 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} diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/Codegen/document/architecture.tex --- 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} diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/Codegen/document/build --- 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" diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/Codegen/document/root.tex --- 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} diff -r c08bd0a219f8 -r e7296939fec2 src/Doc/ROOT --- 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"