author | wenzelm |
Wed, 31 Jul 2019 19:50:38 +0200 | |
changeset 70451 | 550a5a822edb |
parent 68918 | 3a0db30e5d87 |
child 76670 | b04d45bebbc5 |
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 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
13 |
ML \<open> |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
14 |
#allStruct ML_Name_Space.global () |> List.app (fn (name, _) => |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
15 |
if member (op =) ML_Name_Space.hidden_structures name then |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
16 |
ML (Input.string ("structure " ^ name ^ " = " ^ name)) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
17 |
else ()); |
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
18 |
structure Output_Primitives = Output_Primitives_Virtual; |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
19 |
structure Thread_Data = Thread_Data_Virtual; |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
20 |
structure PolyML = PolyML; |
68918
3a0db30e5d87
simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents:
68819
diff
changeset
|
21 |
fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = (); |
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
22 |
|
68819 | 23 |
Proofterm.proofs := 0; |
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
24 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
25 |
Context.setmp_generic_context NONE |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
26 |
ML \<open> |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
27 |
List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
28 |
structure PolyML = |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
29 |
struct |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
30 |
val pointerEq = pointer_eq; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
31 |
structure IntInf = PolyML.IntInf; |
68918
3a0db30e5d87
simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents:
68819
diff
changeset
|
32 |
datatype context = datatype PolyML.context; |
3a0db30e5d87
simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents:
68819
diff
changeset
|
33 |
datatype pretty = datatype PolyML.pretty; |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
34 |
end; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
35 |
\<close> |
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
36 |
\<close> |
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62930
diff
changeset
|
37 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
38 |
setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close> |
68819 | 39 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68812
diff
changeset
|
40 |
declare [[ML_read_global = false]] |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
41 |
|
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff
changeset
|
42 |
end |