author | wenzelm |
Thu, 14 Dec 2017 21:40:43 +0100 | |
changeset 67206 | b8f30228a55b |
parent 67205 | 06c91eac25f2 |
child 68918 | 3a0db30e5d87 |
permissions | -rw-r--r-- |
67205 | 1 |
(* Title: Pure/ML/ml_init.ML |
62818 | 2 |
Author: Makarius |
3 |
||
67205 | 4 |
Initial 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; |
|
67206
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
34 |
|
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
35 |
structure String = |
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
36 |
struct |
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
37 |
open String; |
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
38 |
fun substring (s, i, n) = |
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
39 |
if n = 1 then String.str (String.sub (s, i)) |
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
40 |
else String.substring (s, i, n); |
b8f30228a55b
minor performance tuning, notably for Library.fold_string etc.;
wenzelm
parents:
67205
diff
changeset
|
41 |
end; |