equal
deleted
inserted
replaced
6 |
6 |
7 use "ML-Systems/polyml.ML"; |
7 use "ML-Systems/polyml.ML"; |
8 use "ML-Systems/multithreading_polyml.ML"; |
8 use "ML-Systems/multithreading_polyml.ML"; |
9 |
9 |
10 val pointer_eq = PolyML.pointerEq; |
10 val pointer_eq = PolyML.pointerEq; |
|
11 |
|
12 |
|
13 (* single-threaded profiling *) |
|
14 |
|
15 local val profile_orig = profile in |
|
16 |
|
17 fun profile 0 f x = f x |
|
18 | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x); |
|
19 |
|
20 end; |
11 |
21 |
12 |
22 |
13 (* improved versions of use_text/file *) |
23 (* improved versions of use_text/file *) |
14 |
24 |
15 fun use_text (tune: string -> string) name (print, err) verbose txt = |
25 fun use_text (tune: string -> string) name (print, err) verbose txt = |