src/Pure/ML/ml_pervasive.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 63925 500646ef617a
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62943
     1
(*  Title:      Pure/ML/ml_pervasive.ML
wenzelm@62818
     2
    Author:     Makarius
wenzelm@62818
     3
wenzelm@62943
     4
Initial pervasive ML environment.
wenzelm@62818
     5
*)
wenzelm@62818
     6
wenzelm@62823
     7
structure PolyML_Pretty =
wenzelm@62823
     8
struct
wenzelm@62823
     9
  datatype context = datatype PolyML.context;
wenzelm@62823
    10
  datatype pretty = datatype PolyML.pretty;
wenzelm@62823
    11
end;
wenzelm@62823
    12
wenzelm@62818
    13
val seconds = Time.fromReal;
wenzelm@62818
    14
wenzelm@62818
    15
val _ =
wenzelm@62818
    16
  List.app ML_Name_Space.forget_val
wenzelm@62818
    17
    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
wenzelm@62818
    18
wenzelm@62818
    19
val ord = SML90.ord;
wenzelm@62818
    20
val chr = SML90.chr;
wenzelm@62818
    21
val raw_explode = SML90.explode;
wenzelm@63925
    22
val implode = String.concat;
wenzelm@62818
    23
wenzelm@62818
    24
val pointer_eq = PolyML.pointerEq;
wenzelm@62818
    25
wenzelm@62818
    26
val error_depth = PolyML.error_depth;
wenzelm@62818
    27
wenzelm@62818
    28
open Thread;
wenzelm@62923
    29
wenzelm@62923
    30
datatype illegal = Interrupt;
wenzelm@62923
    31
wenzelm@62923
    32
structure Basic_Exn: BASIC_EXN = Exn;
wenzelm@62923
    33
open Basic_Exn;