equal
deleted
inserted
replaced
1 (* Title: Pure/ML/ml_pervasive.ML |
|
2 Author: Makarius |
|
3 |
|
4 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 = SML90.implode; |
|
23 |
|
24 val pointer_eq = PolyML.pointerEq; |
|
25 |
|
26 val error_depth = PolyML.error_depth; |
|
27 |
|
28 open Thread; |
|