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;
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@67105
    11
external_file "$POLYML_EXE"
wenzelm@67105
    12
wenzelm@67105
    13
wenzelm@62944
    14
subsection \<open>Standard ML environment for virtual bootstrap\<close>
wenzelm@62944
    15
wenzelm@62873
    16
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
wenzelm@62930
    17
wenzelm@62930
    18
SML_import \<open>
wenzelm@62944
    19
  structure Output_Primitives = Output_Primitives_Virtual;
wenzelm@62944
    20
  structure Thread_Data = Thread_Data_Virtual;
wenzelm@64331
    21
  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
wenzelm@62930
    22
\<close>
wenzelm@62930
    23
wenzelm@62944
    24
wenzelm@62944
    25
subsection \<open>Final setup of global ML environment\<close>
wenzelm@62944
    26
wenzelm@62944
    27
ML \<open>Proofterm.proofs := 0\<close>
wenzelm@62944
    28
wenzelm@62944
    29
ML \<open>
wenzelm@62944
    30
  Context.setmp_generic_context NONE
wenzelm@62944
    31
    ML \<open>
wenzelm@62944
    32
      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
wenzelm@62944
    33
      structure PolyML = struct structure IntInf = PolyML.IntInf end;
wenzelm@62944
    34
    \<close>
wenzelm@62944
    35
\<close>
wenzelm@62944
    36
wenzelm@62944
    37
ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
wenzelm@62944
    38
wenzelm@62944
    39
wenzelm@62944
    40
subsection \<open>Switch to bootstrap environment\<close>
wenzelm@62944
    41
wenzelm@62902
    42
setup \<open>Config.put_global ML_Env.SML_environment true\<close>
wenzelm@62868
    43
wenzelm@62868
    44
end