src/Pure/ML_Bootstrap.thy
author paulson <lp15@cam.ac.uk>
Sun, 20 May 2018 18:37:34 +0100
changeset 68239 0764ee22a4d1
parent 67147 dea94b1aabc3
child 68803 169bf32b35dd
permissions -rw-r--r--
tidy up of Derivative
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62887
6b2c60ebd915 clarified ML bootstrap environment;
wenzelm
parents: 62883
diff changeset
     1
(*  Title:      Pure/ML_Bootstrap.thy
62868
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
     3
62887
6b2c60ebd915 clarified ML bootstrap environment;
wenzelm
parents: 62883
diff changeset
     4
ML bootstrap environment -- with access to low-level structures!
62868
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
     5
*)
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
     6
62887
6b2c60ebd915 clarified ML bootstrap environment;
wenzelm
parents: 62883
diff changeset
     7
theory ML_Bootstrap
62880
76e7d9169b54 clarified files;
wenzelm
parents: 62873
diff changeset
     8
imports Pure
62868
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
     9
begin
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
    10
67105
05ff3e6dbbce clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
wenzelm
parents: 64331
diff changeset
    11
external_file "$POLYML_EXE"
05ff3e6dbbce clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
wenzelm
parents: 64331
diff changeset
    12
05ff3e6dbbce clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
wenzelm
parents: 64331
diff changeset
    13
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    14
subsection \<open>Standard ML environment for virtual bootstrap\<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    15
62873
2f9c8a18f832 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents: 62871
diff changeset
    16
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62902
diff changeset
    17
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62902
diff changeset
    18
SML_import \<open>
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    19
  structure Output_Primitives = Output_Primitives_Virtual;
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    20
  structure Thread_Data = Thread_Data_Virtual;
64331
abf7b6e6865f proper type for Poly/ML development version;
wenzelm
parents: 63220
diff changeset
    21
  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62902
diff changeset
    22
\<close>
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62902
diff changeset
    23
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    24
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    25
subsection \<open>Final setup of global ML environment\<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    26
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    27
ML \<open>Proofterm.proofs := 0\<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    28
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    29
ML \<open>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    30
  Context.setmp_generic_context NONE
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    31
    ML \<open>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    32
      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    33
      structure PolyML = struct structure IntInf = PolyML.IntInf end;
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    34
    \<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    35
\<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    36
67147
dea94b1aabc3 prefer control symbol antiquotations;
wenzelm
parents: 67105
diff changeset
    37
ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    38
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    39
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    40
subsection \<open>Switch to bootstrap environment\<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    41
62902
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents: 62893
diff changeset
    42
setup \<open>Config.put_global ML_Env.SML_environment true\<close>
62868
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
    43
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
    44
end