clarified file name;
authorwenzelm
Thu Dec 14 21:31:54 2017 +0100 (17 months ago)
changeset 6720506c91eac25f2
parent 67204 849a838f7e57
child 67206 b8f30228a55b
clarified file name;
src/Pure/ML/ml_init.ML
src/Pure/ML/ml_pervasive.ML
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/ml_init.ML	Thu Dec 14 21:31:54 2017 +0100
     1.3 @@ -0,0 +1,33 @@
     1.4 +(*  Title:      Pure/ML/ml_init.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Initial ML environment.
     1.8 +*)
     1.9 +
    1.10 +structure PolyML_Pretty =
    1.11 +struct
    1.12 +  datatype context = datatype PolyML.context;
    1.13 +  datatype pretty = datatype PolyML.pretty;
    1.14 +end;
    1.15 +
    1.16 +val seconds = Time.fromReal;
    1.17 +
    1.18 +val _ =
    1.19 +  List.app ML_Name_Space.forget_val
    1.20 +    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    1.21 +
    1.22 +val ord = SML90.ord;
    1.23 +val chr = SML90.chr;
    1.24 +val raw_explode = SML90.explode;
    1.25 +val implode = String.concat;
    1.26 +
    1.27 +val pointer_eq = PolyML.pointerEq;
    1.28 +
    1.29 +val error_depth = PolyML.error_depth;
    1.30 +
    1.31 +open Thread;
    1.32 +
    1.33 +datatype illegal = Interrupt;
    1.34 +
    1.35 +structure Basic_Exn: BASIC_EXN = Exn;
    1.36 +open Basic_Exn;
     2.1 --- a/src/Pure/ML/ml_pervasive.ML	Thu Dec 14 21:15:04 2017 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,33 +0,0 @@
     2.4 -(*  Title:      Pure/ML/ml_pervasive.ML
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Initial pervasive ML environment.
     2.8 -*)
     2.9 -
    2.10 -structure PolyML_Pretty =
    2.11 -struct
    2.12 -  datatype context = datatype PolyML.context;
    2.13 -  datatype pretty = datatype PolyML.pretty;
    2.14 -end;
    2.15 -
    2.16 -val seconds = Time.fromReal;
    2.17 -
    2.18 -val _ =
    2.19 -  List.app ML_Name_Space.forget_val
    2.20 -    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    2.21 -
    2.22 -val ord = SML90.ord;
    2.23 -val chr = SML90.chr;
    2.24 -val raw_explode = SML90.explode;
    2.25 -val implode = String.concat;
    2.26 -
    2.27 -val pointer_eq = PolyML.pointerEq;
    2.28 -
    2.29 -val error_depth = PolyML.error_depth;
    2.30 -
    2.31 -open Thread;
    2.32 -
    2.33 -datatype illegal = Interrupt;
    2.34 -
    2.35 -structure Basic_Exn: BASIC_EXN = Exn;
    2.36 -open Basic_Exn;
     3.1 --- a/src/Pure/ROOT.ML	Thu Dec 14 21:15:04 2017 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Thu Dec 14 21:31:54 2017 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  
     3.5  section "Bootstrap phase 0: Poly/ML setup";
     3.6  
     3.7 -ML_file "ML/ml_pervasive.ML";
     3.8 +ML_file "ML/ml_init.ML";
     3.9  ML_file "ML/ml_system.ML";
    3.10  ML_file "System/distribution.ML";
    3.11