Theory ML_Bootstrap

theory ML_Bootstrap
imports Pure
(*  Title:      Pure/ML_Bootstrap.thy
    Author:     Makarius

ML bootstrap environment -- with access to low-level structures!

theory ML_Bootstrap
imports Pure

external_file "$POLYML_EXE"

subsection ‹Standard ML environment for virtual bootstrap›

setup ‹Context.theory_map ML_Env.init_bootstrap›

SML_import ‹
  structure Output_Primitives = Output_Primitives_Virtual;
  structure Thread_Data = Thread_Data_Virtual;
  fun ML_system_pp (_: -> 'a -> 'b -> PolyML_Pretty.pretty) = ();

subsection ‹Final setup of global ML environment›

ML ‹Proofterm.proofs := 0›

ML ‹
  Context.setmp_generic_context NONE
    ML ‹ ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
      structure PolyML = struct structure IntInf = PolyML.IntInf end;

ML ‹\<^assert> (not (can ML ‹open RunCall›))›

subsection ‹Switch to bootstrap environment›

setup ‹Config.put_global ML_Env.SML_environment true›