diff -r 3a1aef73b2b2 -r aea5d7fa7ef5 doc-src/Codegen/codegen_process.ps
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/codegen_process.ps	Wed Mar 04 11:05:29 2009 +0100
@@ -0,0 +1,586 @@
+%!PS-Adobe-2.0
+%%Creator: dot version 2.2 (Mon Sep 12 23:33:36 UTC 2005)
+%%For: (haftmann) Florian Haftmann
+%%Title: _anonymous_0
+%%Pages: (atend)
+%%BoundingBox: 35 35 451 291
+%%EndComments
+save
+%%BeginProlog
+/DotDict 200 dict def
+DotDict begin
+
+/setupLatin1 {
+mark
+/EncodingVector 256 array def
+ EncodingVector 0
+
+ISOLatin1Encoding 0 255 getinterval putinterval
+
+EncodingVector
+  dup 306 /AE
+  dup 301 /Aacute
+  dup 302 /Acircumflex
+  dup 304 /Adieresis
+  dup 300 /Agrave
+  dup 305 /Aring
+  dup 303 /Atilde
+  dup 307 /Ccedilla
+  dup 311 /Eacute
+  dup 312 /Ecircumflex
+  dup 313 /Edieresis
+  dup 310 /Egrave
+  dup 315 /Iacute
+  dup 316 /Icircumflex
+  dup 317 /Idieresis
+  dup 314 /Igrave
+  dup 334 /Udieresis
+  dup 335 /Yacute
+  dup 376 /thorn
+  dup 337 /germandbls
+  dup 341 /aacute
+  dup 342 /acircumflex
+  dup 344 /adieresis
+  dup 346 /ae
+  dup 340 /agrave
+  dup 345 /aring
+  dup 347 /ccedilla
+  dup 351 /eacute
+  dup 352 /ecircumflex
+  dup 353 /edieresis
+  dup 350 /egrave
+  dup 355 /iacute
+  dup 356 /icircumflex
+  dup 357 /idieresis
+  dup 354 /igrave
+  dup 360 /dcroat
+  dup 361 /ntilde
+  dup 363 /oacute
+  dup 364 /ocircumflex
+  dup 366 /odieresis
+  dup 362 /ograve
+  dup 365 /otilde
+  dup 370 /oslash
+  dup 372 /uacute
+  dup 373 /ucircumflex
+  dup 374 /udieresis
+  dup 371 /ugrave
+  dup 375 /yacute
+  dup 377 /ydieresis  
+
+% Set up ISO Latin 1 character encoding
+/starnetISO {
+        dup dup findfont dup length dict begin
+        { 1 index /FID ne { def }{ pop pop } ifelse
+        } forall
+        /Encoding EncodingVector def
+        currentdict end definefont
+} def
+/Times-Roman starnetISO def
+/Times-Italic starnetISO def
+/Times-Bold starnetISO def
+/Times-BoldItalic starnetISO def
+/Helvetica starnetISO def
+/Helvetica-Oblique starnetISO def
+/Helvetica-Bold starnetISO def
+/Helvetica-BoldOblique starnetISO def
+/Courier starnetISO def
+/Courier-Oblique starnetISO def
+/Courier-Bold starnetISO def
+/Courier-BoldOblique starnetISO def
+cleartomark
+} bind def
+
+%%BeginResource: procset graphviz 0 0
+/coord-font-family /Times-Roman def
+/default-font-family /Times-Roman def
+/coordfont coord-font-family findfont 8 scalefont def
+
+/InvScaleFactor 1.0 def
+/set_scale {
+	dup 1 exch div /InvScaleFactor exch def
+	dup scale
+} bind def
+
+% styles
+/solid { [] 0 setdash } bind def
+/dashed { [9 InvScaleFactor mul dup ] 0 setdash } bind def
+/dotted { [1 InvScaleFactor mul 6 InvScaleFactor mul] 0 setdash } bind def
+/invis {/fill {newpath} def /stroke {newpath} def /show {pop newpath} def} bind def
+/bold { 2 setlinewidth } bind def
+/filled { } bind def
+/unfilled { } bind def
+/rounded { } bind def
+/diagonals { } bind def
+
+% hooks for setting color 
+/nodecolor { sethsbcolor } bind def
+/edgecolor { sethsbcolor } bind def
+/graphcolor { sethsbcolor } bind def
+/nopcolor {pop pop pop} bind def
+
+/beginpage {	% i j npages
+	/npages exch def
+	/j exch def
+	/i exch def
+	/str 10 string def
+	npages 1 gt {
+		gsave
+			coordfont setfont
+			0 0 moveto
+			(\() show i str cvs show (,) show j str cvs show (\)) show
+		grestore
+	} if
+} bind def
+
+/set_font {
+	findfont exch
+	scalefont setfont
+} def
+
+% draw aligned label in bounding box aligned to current point
+/alignedtext {			% width adj text
+	/text exch def
+	/adj exch def
+	/width exch def
+	gsave
+		width 0 gt {
+			text stringwidth pop adj mul 0 rmoveto
+		} if
+		[] 0 setdash
+		text show
+	grestore
+} def
+
+/boxprim {				% xcorner ycorner xsize ysize
+		4 2 roll
+		moveto
+		2 copy
+		exch 0 rlineto
+		0 exch rlineto
+		pop neg 0 rlineto
+		closepath
+} bind def
+
+/ellipse_path {
+	/ry exch def
+	/rx exch def
+	/y exch def
+	/x exch def
+	matrix currentmatrix
+	newpath
+	x y translate
+	rx ry scale
+	0 0 1 0 360 arc
+	setmatrix
+} bind def
+
+/endpage { showpage } bind def
+/showpage { } def
+
+/layercolorseq
+	[	% layer color sequence - darkest to lightest
+		[0 0 0]
+		[.2 .8 .8]
+		[.4 .8 .8]
+		[.6 .8 .8]
+		[.8 .8 .8]
+	]
+def
+
+/layerlen layercolorseq length def
+
+/setlayer {/maxlayer exch def /curlayer exch def
+	layercolorseq curlayer 1 sub layerlen mod get
+	aload pop sethsbcolor
+	/nodecolor {nopcolor} def
+	/edgecolor {nopcolor} def
+	/graphcolor {nopcolor} def
+} bind def
+
+/onlayer { curlayer ne {invis} if } def
+
+/onlayers {
+	/myupper exch def
+	/mylower exch def
+	curlayer mylower lt
+	curlayer myupper gt
+	or
+	{invis} if
+} def
+
+/curlayer 0 def
+
+%%EndResource
+%%EndProlog
+%%BeginSetup
+14 default-font-family set_font
+1 setmiterlimit
+% /arrowlength 10 def
+% /arrowwidth 5 def
+
+% make sure pdfmark is harmless for PS-interpreters other than Distiller
+/pdfmark where {pop} {userdict /pdfmark /cleartomark load put} ifelse
+% make '<<' and '>>' safe on PS Level 1 devices
+/languagelevel where {pop languagelevel}{1} ifelse
+2 lt {
+    userdict (<<) cvn ([) cvn load put
+    userdict (>>) cvn ([) cvn load put
+} if
+
+%%EndSetup
+%%Page: 1 1
+%%PageBoundingBox: 36 36 451 291
+%%PageOrientation: Portrait
+gsave
+35 35 416 256 boxprim clip newpath
+36 36 translate
+0 0 1 beginpage
+0 0 translate 0 rotate
+[ /CropBox [36 36 451 291] /PAGES pdfmark
+0.000 0.000 0.000 graphcolor
+14.00 /Times-Roman set_font
+
+%	theory
+gsave 10 dict begin
+newpath 93 254 moveto
+1 254 lineto
+1 214 lineto
+93 214 lineto
+closepath
+stroke
+gsave 10 dict begin
+8 237 moveto
+(Isabelle/HOL)
+[4.56 5.52 6.24 6.96 6.24 3.84 3.84 6.24 3.84 10.08 10.08 8.64]
+xshow
+16 221 moveto
+(Isar theory)
+[4.56 5.52 6.24 4.56 3.6 4.08 6.96 6.24 6.96 4.8 6.96]
+xshow
+end grestore
+end grestore
+
+%	selection
+gsave 10 dict begin
+183 234 38 18 ellipse_path
+stroke
+gsave 10 dict begin
+158 229 moveto
+(selection)
+[5.52 6.24 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	theory -> selection
+newpath 94 234 moveto
+107 234 121 234 135 234 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 135 238 moveto
+145 234 lineto
+135 231 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 135 238 moveto
+145 234 lineto
+135 231 lineto
+closepath
+stroke
+end grestore
+
+%	sml
+gsave 10 dict begin
+newpath 74 144 moveto
+20 144 lineto
+20 108 lineto
+74 108 lineto
+closepath
+stroke
+gsave 10 dict begin
+32 121 moveto
+(SML)
+[7.68 12.48 8.64]
+xshow
+end grestore
+end grestore
+
+%	other
+gsave 10 dict begin
+gsave 10 dict begin
+41 67 moveto
+(...)
+[3.6 3.6 3.6]
+xshow
+end grestore
+end grestore
+
+%	haskell
+gsave 10 dict begin
+newpath 77 36 moveto
+17 36 lineto
+17 0 lineto
+77 0 lineto
+closepath
+stroke
+gsave 10 dict begin
+25 13 moveto
+(Haskell)
+[10.08 6.24 5.52 6.72 6.24 3.84 3.84]
+xshow
+end grestore
+end grestore
+
+%	preprocessing
+gsave 10 dict begin
+183 180 52 18 ellipse_path
+stroke
+gsave 10 dict begin
+143 175 moveto
+(preprocessing)
+[6.96 4.56 6.24 6.96 4.56 6.96 6.24 6.24 5.52 5.52 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	selection -> preprocessing
+newpath 183 216 moveto
+183 213 183 211 183 208 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 187 208 moveto
+183 198 lineto
+180 208 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 187 208 moveto
+183 198 lineto
+180 208 lineto
+closepath
+stroke
+end grestore
+
+%	def_eqn
+gsave 10 dict begin
+newpath 403 198 moveto
+283 198 lineto
+283 162 lineto
+403 162 lineto
+closepath
+stroke
+gsave 10 dict begin
+291 175 moveto
+(defining equations)
+[6.96 6.24 4.8 3.84 6.96 3.84 6.96 6.96 3.6 6.24 6.72 6.96 6.24 3.84 3.84 6.96 6.96 5.52]
+xshow
+end grestore
+end grestore
+
+%	preprocessing -> def_eqn
+newpath 236 180 moveto
+248 180 260 180 273 180 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 273 184 moveto
+283 180 lineto
+273 177 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 273 184 moveto
+283 180 lineto
+273 177 lineto
+closepath
+stroke
+end grestore
+
+%	serialization
+gsave 10 dict begin
+183 72 47 18 ellipse_path
+stroke
+gsave 10 dict begin
+148 67 moveto
+(serialization)
+[5.52 6.24 4.8 3.84 6.24 3.84 3.84 6.24 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	serialization -> sml
+newpath 150 85 moveto
+129 93 104 103 83 111 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 82 108 moveto
+74 115 lineto
+85 114 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 82 108 moveto
+74 115 lineto
+85 114 lineto
+closepath
+stroke
+end grestore
+
+%	serialization -> other
+gsave 10 dict begin
+dotted
+newpath 135 72 moveto
+119 72 100 72 84 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 84 69 moveto
+74 72 lineto
+84 76 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 84 69 moveto
+74 72 lineto
+84 76 lineto
+closepath
+stroke
+end grestore
+end grestore
+
+%	serialization -> haskell
+newpath 150 59 moveto
+131 51 107 42 86 34 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 88 31 moveto
+77 30 lineto
+85 37 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 88 31 moveto
+77 30 lineto
+85 37 lineto
+closepath
+stroke
+end grestore
+
+%	translation
+gsave 10 dict begin
+343 126 43 18 ellipse_path
+stroke
+gsave 10 dict begin
+313 121 moveto
+(translation)
+[3.84 4.56 6.24 6.96 5.52 3.84 6.24 3.84 3.84 6.96 6.96]
+xshow
+end grestore
+end grestore
+
+%	def_eqn -> translation
+newpath 343 162 moveto
+343 159 343 157 343 154 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 347 154 moveto
+343 144 lineto
+340 154 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 347 154 moveto
+343 144 lineto
+340 154 lineto
+closepath
+stroke
+end grestore
+
+%	iml
+gsave 10 dict begin
+newpath 413 90 moveto
+273 90 lineto
+273 54 lineto
+413 54 lineto
+closepath
+stroke
+gsave 10 dict begin
+280 67 moveto
+(intermediate language)
+[3.84 6.96 3.84 6.24 4.8 10.8 6.24 6.96 3.84 6.24 3.84 6.24 3.6 3.84 6.24 6.96 6.96 6.96 6.24 6.72 6.24]
+xshow
+end grestore
+end grestore
+
+%	translation -> iml
+newpath 343 108 moveto
+343 105 343 103 343 100 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 347 100 moveto
+343 90 lineto
+340 100 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 347 100 moveto
+343 90 lineto
+340 100 lineto
+closepath
+stroke
+end grestore
+
+%	iml -> serialization
+newpath 272 72 moveto
+262 72 251 72 241 72 curveto
+stroke
+gsave 10 dict begin
+solid
+1 setlinewidth
+0.000 0.000 0.000 edgecolor
+newpath 241 69 moveto
+231 72 lineto
+241 76 lineto
+closepath
+fill
+0.000 0.000 0.000 edgecolor
+newpath 241 69 moveto
+231 72 lineto
+241 76 lineto
+closepath
+stroke
+end grestore
+endpage
+showpage
+grestore
+%%PageTrailer
+%%EndPage: 1
+%%Trailer
+%%Pages: 1
+end
+restore
+%%EOF