src/Pure/ML_Bootstrap.thy
author wenzelm
Wed, 31 Jul 2019 19:50:38 +0200
changeset 70451 550a5a822edb
parent 68918 3a0db30e5d87
child 76670 b04d45bebbc5
permissions -rw-r--r--
clarified export: retain proof boxes as local definitions -- more scalable;
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
68816
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    13
ML \<open>
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    14
  #allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    15
    if member (op =) ML_Name_Space.hidden_structures name then
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    16
      ML (Input.string ("structure " ^ name ^ " = " ^ name))
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    17
    else ());
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    18
  structure Output_Primitives = Output_Primitives_Virtual;
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    19
  structure Thread_Data = Thread_Data_Virtual;
68816
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    20
  structure PolyML = PolyML;
68918
3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents: 68819
diff changeset
    21
  fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = ();
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    22
68819
wenzelm
parents: 68816
diff changeset
    23
  Proofterm.proofs := 0;
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    24
68816
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    25
  Context.setmp_generic_context NONE
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    26
    ML \<open>
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    27
      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    28
      structure PolyML =
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    29
      struct
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    30
        val pointerEq = pointer_eq;
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    31
        structure IntInf = PolyML.IntInf;
68918
3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents: 68819
diff changeset
    32
        datatype context = datatype PolyML.context;
3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents: 68819
diff changeset
    33
        datatype pretty = datatype PolyML.pretty;
68816
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    34
      end;
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    35
    \<close>
62944
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    36
\<close>
3ee643c5ed00 more standard session build process, including browser_info;
wenzelm
parents: 62930
diff changeset
    37
68816
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    38
setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
68819
wenzelm
parents: 68816
diff changeset
    39
68816
5a53724fe247 support named ML environments, notably "Isabelle", "SML";
wenzelm
parents: 68812
diff changeset
    40
declare [[ML_read_global = false]]
62868
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
    41
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset
    42
end