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;
     1 (*  Title:      Pure/ML/ml_pervasive.ML
     2     Author:     Makarius
     3 
     4 Initial pervasive ML environment.
     5 *)
     6 
     7 structure PolyML_Pretty =
     8 struct
     9   datatype context = datatype PolyML.context;
    10   datatype pretty = datatype PolyML.pretty;
    11 end;
    12 
    13 val seconds = Time.fromReal;
    14 
    15 val _ =
    16   List.app ML_Name_Space.forget_val
    17     ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
    18 
    19 val ord = SML90.ord;
    20 val chr = SML90.chr;
    21 val raw_explode = SML90.explode;
    22 val implode = String.concat;
    23 
    24 val pointer_eq = PolyML.pointerEq;
    25 
    26 val error_depth = PolyML.error_depth;
    27 
    28 open Thread;
    29 
    30 datatype illegal = Interrupt;
    31 
    32 structure Basic_Exn: BASIC_EXN = Exn;
    33 open Basic_Exn;