author | paulson <lp15@cam.ac.uk> |
Sun, 20 May 2018 18:37:34 +0100 | |
changeset 68239 | 0764ee22a4d1 |
parent 67147 | dea94b1aabc3 |
child 68803 | 169bf32b35dd |
permissions | -rw-r--r-- |
62887 | 1 |
(* Title: Pure/ML_Bootstrap.thy |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
3 |
|
62887 | 4 |
ML bootstrap environment -- with access to low-level structures! |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
5 |
*) |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
6 |
|
62887 | 7 |
theory ML_Bootstrap |
62880 | 8 |
imports Pure |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
9 |
begin |
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
10 |
|
67105
05ff3e6dbbce
clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
wenzelm
parents:
64331
diff
changeset
|
11 |
external_file "$POLYML_EXE" |
05ff3e6dbbce
clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
wenzelm
parents:
64331
diff
changeset
|
12 |
|
05ff3e6dbbce
clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
wenzelm
parents:
64331
diff
changeset
|
13 |
|
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
14 |
subsection \<open>Standard ML environment for virtual bootstrap\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
15 |
|
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62871
diff
changeset
|
16 |
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62902
diff
changeset
|
17 |
|
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62902
diff
changeset
|
18 |
SML_import \<open> |
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
19 |
structure Output_Primitives = Output_Primitives_Virtual; |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
20 |
structure Thread_Data = Thread_Data_Virtual; |
64331 | 21 |
fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = (); |
62930
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62902
diff
changeset
|
22 |
\<close> |
51ac6bc389e8
shared output primitives of physical/virtual Pure;
wenzelm
parents:
62902
diff
changeset
|
23 |
|
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
24 |
|
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
25 |
subsection \<open>Final setup of global ML environment\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
26 |
|
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
27 |
ML \<open>Proofterm.proofs := 0\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
28 |
|
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
29 |
ML \<open> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
30 |
Context.setmp_generic_context NONE |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
31 |
ML \<open> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
32 |
List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures; |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
33 |
structure PolyML = struct structure IntInf = PolyML.IntInf end; |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
34 |
\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
35 |
\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
36 |
|
67147 | 37 |
ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close> |
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
38 |
|
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
39 |
|
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
40 |
subsection \<open>Switch to bootstrap environment\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
41 |
|
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62893
diff
changeset
|
42 |
setup \<open>Config.put_global ML_Env.SML_environment true\<close> |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
43 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
44 |
end |