equal
deleted
inserted
replaced
27 val implode = SML90.implode; |
27 val implode = SML90.implode; |
28 |
28 |
29 (* compiler-independent timing functions *) |
29 (* compiler-independent timing functions *) |
30 |
30 |
31 use "ML-Systems/cpu-timer-basis.ML"; |
31 use "ML-Systems/cpu-timer-basis.ML"; |
|
32 |
|
33 (* bounded time execution *) |
|
34 |
|
35 use "ML-Systems/polyml-time-limit.ML"; |
32 |
36 |
33 (* prompts *) |
37 (* prompts *) |
34 |
38 |
35 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
39 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
36 |
40 |