62943
|
1 |
(* Title: Pure/ML/ml_pervasive.ML
|
62818
|
2 |
Author: Makarius
|
|
3 |
|
62943
|
4 |
Initial pervasive ML environment.
|
62818
|
5 |
*)
|
|
6 |
|
62823
|
7 |
structure PolyML_Pretty =
|
|
8 |
struct
|
|
9 |
datatype context = datatype PolyML.context;
|
|
10 |
datatype pretty = datatype PolyML.pretty;
|
|
11 |
end;
|
|
12 |
|
62818
|
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;
|
63925
|
22 |
val implode = String.concat;
|
62818
|
23 |
|
|
24 |
val pointer_eq = PolyML.pointerEq;
|
|
25 |
|
|
26 |
val error_depth = PolyML.error_depth;
|
|
27 |
|
|
28 |
open Thread;
|
62923
|
29 |
|
|
30 |
datatype illegal = Interrupt;
|
|
31 |
|
|
32 |
structure Basic_Exn: BASIC_EXN = Exn;
|
|
33 |
open Basic_Exn;
|