1 (* Title: Pure/ML-Systems/polyml_common.ML |
|
2 |
|
3 Compatibility file for Poly/ML -- common part for 5.x. |
|
4 *) |
|
5 |
|
6 fun op before (a, _: unit) = a; |
|
7 |
|
8 exception Interrupt = SML90.Interrupt; |
|
9 |
|
10 use "General/exn.ML"; |
|
11 |
|
12 if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ()) |
|
13 then () |
|
14 else use "ML-Systems/single_assignment_polyml.ML"; |
|
15 |
|
16 use "ML-Systems/multithreading.ML"; |
|
17 use "ML-Systems/ml_pretty.ML"; |
|
18 use "ML-Systems/use_context.ML"; |
|
19 |
|
20 val seconds = Time.fromReal; |
|
21 |
|
22 |
|
23 |
|
24 (** ML system and platform related **) |
|
25 |
|
26 val _ = PolyML.Compiler.forgetValue "isSome"; |
|
27 val _ = PolyML.Compiler.forgetValue "getOpt"; |
|
28 val _ = PolyML.Compiler.forgetValue "valOf"; |
|
29 val _ = PolyML.Compiler.forgetValue "foldl"; |
|
30 val _ = PolyML.Compiler.forgetValue "foldr"; |
|
31 val _ = PolyML.Compiler.forgetValue "print"; |
|
32 val _ = PolyML.Compiler.forgetValue "explode"; |
|
33 val _ = PolyML.Compiler.forgetValue "concat"; |
|
34 |
|
35 |
|
36 (* Compiler options *) |
|
37 |
|
38 PolyML.Compiler.printInAlphabeticalOrder := false; |
|
39 PolyML.Compiler.maxInlineSize := 80; |
|
40 |
|
41 |
|
42 (* old Poly/ML emulation *) |
|
43 |
|
44 fun quit () = exit 0; |
|
45 |
|
46 |
|
47 (* restore old-style character / string functions *) |
|
48 |
|
49 val ord = SML90.ord; |
|
50 val chr = SML90.chr; |
|
51 val raw_explode = SML90.explode; |
|
52 val implode = SML90.implode; |
|
53 |
|
54 |
|
55 (* prompts *) |
|
56 |
|
57 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); |
|
58 |
|
59 |
|
60 (* toplevel printing *) |
|
61 |
|
62 local |
|
63 val depth = ref 10; |
|
64 in |
|
65 fun get_print_depth () = ! depth; |
|
66 fun print_depth n = (depth := n; PolyML.print_depth n); |
|
67 end; |
|
68 |
|
69 val error_depth = PolyML.error_depth; |
|
70 |
|
71 val ml_make_string = "PolyML.makestring"; |
|
72 |
|
73 |
|
74 |
|
75 (** Runtime system **) |
|
76 |
|
77 val exception_trace = PolyML.exception_trace; |
|
78 val timing = PolyML.timing; |
|
79 val profiling = PolyML.profiling; |
|
80 |
|
81 fun profile 0 f x = f x |
|
82 | profile n f x = |
|
83 let |
|
84 val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; |
|
85 val res = Exn.capture f x; |
|
86 val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; |
|
87 in Exn.release res end; |
|
88 |
|