| author | haftmann |
| Fri, 24 Apr 2009 17:45:17 +0200 | |
| changeset 30973 | 304ab57afa6e |
| parent 30929 | d9343c0aac11 |
| child 31036 | 64ff53fc0c0c |
| permissions | -rw-r--r-- |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
1 |
(* Title: Tools/Code_Generator.thy |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
3 |
*) |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
4 |
|
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
5 |
header {* Loading the code generator modules *}
|
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
6 |
|
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
7 |
theory Code_Generator |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
8 |
imports Pure |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
9 |
uses |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
10 |
"~~/src/Tools/value.ML" |
|
30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30929
diff
changeset
|
11 |
"~~/src/Tools/quickcheck.ML" |
|
30929
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
12 |
"~~/src/Tools/code/code_name.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
13 |
"~~/src/Tools/code/code_wellsorted.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
14 |
"~~/src/Tools/code/code_thingol.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
15 |
"~~/src/Tools/code/code_printer.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
16 |
"~~/src/Tools/code/code_target.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
17 |
"~~/src/Tools/code/code_ml.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
18 |
"~~/src/Tools/code/code_haskell.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
19 |
"~~/src/Tools/nbe.ML" |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
20 |
begin |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
21 |
|
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
22 |
setup {*
|
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
23 |
Code_ML.setup |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
24 |
#> Code_Haskell.setup |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
25 |
#> Nbe.setup |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
26 |
*} |
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
27 |
|
|
d9343c0aac11
code generator bootstrap theory src/Tools/Code_Generator.thy
haftmann
parents:
diff
changeset
|
28 |
end |