src/Pure/ML_Bootstrap.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 67105 05ff3e6dbbce
child 67147 dea94b1aabc3
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/ML_Bootstrap.thy
     2     Author:     Makarius
     3 
     4 ML bootstrap environment -- with access to low-level structures!
     5 *)
     6 
     7 theory ML_Bootstrap
     8 imports Pure
     9 begin
    10 
    11 external_file "$POLYML_EXE"
    12 
    13 
    14 subsection \<open>Standard ML environment for virtual bootstrap\<close>
    15 
    16 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
    17 
    18 SML_import \<open>
    19   structure Output_Primitives = Output_Primitives_Virtual;
    20   structure Thread_Data = Thread_Data_Virtual;
    21   fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
    22 \<close>
    23 
    24 
    25 subsection \<open>Final setup of global ML environment\<close>
    26 
    27 ML \<open>Proofterm.proofs := 0\<close>
    28 
    29 ML \<open>
    30   Context.setmp_generic_context NONE
    31     ML \<open>
    32       List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
    33       structure PolyML = struct structure IntInf = PolyML.IntInf end;
    34     \<close>
    35 \<close>
    36 
    37 ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
    38 
    39 
    40 subsection \<open>Switch to bootstrap environment\<close>
    41 
    42 setup \<open>Config.put_global ML_Env.SML_environment true\<close>
    43 
    44 end