1(*  Title:      Pure/ML_Bootstrap.thy
2    Author:     Makarius
3
4ML bootstrap environment -- with access to low-level structures!
5*)
6
7theory ML_Bootstrap
8imports Pure
9begin
10
11external_file "$POLYML_EXE"
12
13ML \<open>
14  #allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
15    if member (op =) ML_Name_Space.hidden_structures name then
16      ML (Input.string ("structure " ^ name ^ " = " ^ name))
17    else ());
18  structure Output_Primitives = Output_Primitives_Virtual;
19  structure Thread_Data = Thread_Data_Virtual;
20  structure PolyML = PolyML;
21  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = ();
22
23  Proofterm.proofs := 0;
24
25  Context.setmp_generic_context NONE
26    ML \<open>
27      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
28      structure PolyML =
29      struct
30        val pointerEq = pointer_eq;
31        structure IntInf = PolyML.IntInf;
32        datatype context = datatype PolyML.context;
33        datatype pretty = datatype PolyML.pretty;
34      end;
35    \<close>
36\<close>
37
38setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
39
40declare [[ML_read_global = false]]
41
42end
43