1(*  Title:      Pure/ML/ml_init.ML
2    Author:     Makarius
3
4Initial ML environment.
5*)
6
7structure PolyML_Pretty =
8struct
9  datatype context = datatype PolyML.context;
10  datatype pretty = datatype PolyML.pretty;
11end;
12
13val seconds = Time.fromReal;
14
15val _ =
16  List.app ML_Name_Space.forget_val
17    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
18
19val ord = SML90.ord;
20val chr = SML90.chr;
21val raw_explode = SML90.explode;
22val implode = String.concat;
23
24val pointer_eq = PolyML.pointerEq;
25
26val error_depth = PolyML.error_depth;
27
28open Thread;
29
30datatype illegal = Interrupt;
31
32structure Basic_Exn: BASIC_EXN = Exn;
33open Basic_Exn;
34
35structure String =
36struct
37  open String;
38  fun substring (s, i, n) =
39    if n = 1 then String.str (String.sub (s, i))
40    else String.substring (s, i, n);
41end;
42