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