equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/polyml.ML |
1 (* Title: Pure/ML-Systems/polyml.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Compatibility file for Poly/ML (version 4.0). |
6 Compatibility file for Poly/ML (version 4.0, 4.1, 4.1.x). |
7 *) |
7 *) |
8 |
8 |
9 (** ML system related **) |
9 (** ML system related **) |
10 |
10 |
11 (* old Poly/ML emulation *) |
11 (* old Poly/ML emulation *) |
24 val ord = SML90.ord; |
24 val ord = SML90.ord; |
25 val chr = SML90.chr; |
25 val chr = SML90.chr; |
26 val explode = SML90.explode; |
26 val explode = SML90.explode; |
27 val implode = SML90.implode; |
27 val implode = SML90.implode; |
28 |
28 |
|
29 |
29 (* compiler-independent timing functions *) |
30 (* compiler-independent timing functions *) |
30 |
31 |
31 use "ML-Systems/cpu-timer-basis.ML"; |
32 use "ML-Systems/cpu-timer-basis.ML"; |
32 |
33 |
|
34 |
33 (* bounded time execution *) |
35 (* bounded time execution *) |
34 |
36 |
35 use "ML-Systems/polyml-time-limit.ML"; |
37 use "ML-Systems/polyml-time-limit.ML"; |
|
38 |
36 |
39 |
37 (* prompts *) |
40 (* prompts *) |
38 |
41 |
39 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
42 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
40 |
43 |