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