author | paulson |
Fri, 18 Oct 1996 11:32:38 +0200 | |
changeset 2101 | 5d44339454a4 |
parent 2093 | 8e3e56fecfbe |
child 2141 | c2aedd8169cd |
permissions | -rw-r--r-- |
1480 | 1 |
(* Title: Pure/NJ1xx.ML |
2 |
ID: $Id$ |
|
3 |
Author: Carsten Clasohm, TU Muenchen |
|
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Compatibility file for Standard ML of New Jersey version 1.xx. |
|
7 |
*) |
|
8 |
||
9 |
(*** Poly/ML emulation ***) |
|
10 |
||
11 |
||
12 |
(*To exit the system with an exit code -- an alternative to ^D *) |
|
13 |
fun exit 0 = OS.Process.exit OS.Process.success |
|
14 |
| exit _ = OS.Process.exit OS.Process.failure; |
|
15 |
fun quit () = exit 0; |
|
16 |
||
17 |
(*To change the current directory*) |
|
18 |
val cd = OS.FileSys.chDir; |
|
19 |
||
20 |
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) |
|
21 |
fun print_depth n = (Compiler.Control.Print.printDepth := n div 2; |
|
22 |
Compiler.Control.Print.printLength := n); |
|
23 |
||
24 |
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
|
25 |
||
26 |
fun make_pp path pprint = |
|
27 |
let |
|
28 |
open Compiler.PrettyPrint; |
|
29 |
||
30 |
fun pp pps obj = |
|
31 |
pprint obj |
|
32 |
(add_string pps, begin_block pps INCONSISTENT, |
|
33 |
fn wd => add_break pps (wd, 0), fn () => add_newline pps, |
|
34 |
fn () => end_block pps); |
|
35 |
in |
|
36 |
(path, pp) |
|
37 |
end; |
|
38 |
||
39 |
fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp; |
|
40 |
||
41 |
||
42 |
(*** New Jersey ML parameters ***) |
|
43 |
||
44 |
(* Suppresses Garbage Collection messages; doesn't work yet *) |
|
45 |
(*System.Runtime.gc 0;*) |
|
46 |
||
47 |
val _ = (Compiler.Control.Print.printLength := 1000; |
|
48 |
Compiler.Control.Print.printDepth := 350; |
|
49 |
Compiler.Control.Print.stringDepth := 250; |
|
50 |
Compiler.Control.Print.signatures := 2); |
|
51 |
||
52 |
(*** Character/string functions which are compatibel with 0.93 and Poly/ML ***) |
|
53 |
||
54 |
val ord = Char.ord o hd o explode; |
|
55 |
val chr = str o Char.chr; |
|
56 |
val explode = (map str) o String.explode; |
|
57 |
val implode = String.concat; |
|
58 |
||
59 |
||
60 |
(*** Timing functions ***) |
|
61 |
||
62 |
(*A conditional timing function: applies f to () and, if the flag is true, |
|
63 |
prints its runtime. *) |
|
64 |
fun cond_timeit flag f = |
|
65 |
if flag then |
|
2076
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
66 |
let open Time (*...for Time.toString, Time.+ and Time.- *) |
2101
5d44339454a4
Moving the CPUtimer declaration into cond_timeit should
paulson
parents:
2093
diff
changeset
|
67 |
val CPUtimer = Timer.startCPUTimer(); |
5d44339454a4
Moving the CPUtimer declaration into cond_timeit should
paulson
parents:
2093
diff
changeset
|
68 |
val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); |
1480 | 69 |
val result = f(); |
2076
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
70 |
val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) |
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
71 |
in print("User " ^ toString (usrt2-usrt1) ^ |
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
72 |
" GC " ^ toString (gct2-gct1) ^ |
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
73 |
" All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
74 |
" secs\n") |
ec8857a115af
cond_timeit now catches exception Time, which sml/nj
paulson
parents:
1577
diff
changeset
|
75 |
handle Time => (); |
1480 | 76 |
result |
77 |
end |
|
78 |
else f(); |
|
79 |
||
80 |
||
81 |
(*** File handling ***) |
|
82 |
||
83 |
(*Get time of last modification; if file doesn't exist return an empty string*) |
|
84 |
local |
|
85 |
open Timer; |
|
86 |
open Posix.FileSys; |
|
87 |
in |
|
88 |
fun file_info "" = "" |
|
89 |
| file_info name = Time.toString (ST.mtime (stat name)) handle _ => ""; |
|
90 |
||
91 |
val delete_file = unlink; |
|
92 |
end; |
|
93 |
||
94 |
(*Get pathname of current working directory *) |
|
95 |
fun pwd () = OS.FileSys.getDir (); |
|
96 |
||
97 |
||
98 |
(*** ML command execution ***) |
|
99 |
||
100 |
fun use_string commands = |
|
101 |
Compiler.Interact.use_stream (open_string (implode commands)); |
|
102 |
||
103 |
||
104 |
(*** System command execution ***) |
|
105 |
||
106 |
(*Execute an Unix command which doesn't take any input from stdin and |
|
107 |
sends its output to stdout. |
|
108 |
This could be done more easily by Unix.execute, but that function |
|
109 |
doesn't use the PATH.*) |
|
110 |
fun execute command = |
|
111 |
let val tmp_name = "isa_converted.tmp" |
|
112 |
val is = (OS.Process.system (command ^ " > " ^ tmp_name); |
|
113 |
open_in tmp_name); |
|
114 |
val result = input (is, 999999); |
|
115 |
in close_in is; |
|
116 |
delete_file tmp_name; |
|
117 |
result |
|
118 |
end; |
|
119 |
||
120 |
||
121 |
(*For use in Makefiles -- saves space*) |
|
122 |
fun xML filename banner = |
|
123 |
let val runtime = List.hd (SMLofNJ.getAllArgs()) |
|
124 |
val exec_file = IO.open_out filename |
|
1577 | 125 |
|
1480 | 126 |
val _ = IO.output (exec_file, |
127 |
String.concat |
|
128 |
["#!/bin/sh\n", |
|
1577 | 129 |
runtime, " @SMLdebug=/dev/null @SMLload=", filename, |
130 |
".heap\n"]) |
|
131 |
(*"@SMLdebug=..." sends GC messages to /dev/null*) |
|
132 |
||
1480 | 133 |
val _ = IO.close_out exec_file; |
134 |
val _ = OS.Process.system ("chmod a+x " ^ filename) |
|
135 |
in exportML (filename^".heap"); |
|
136 |
print(banner^"\n") |
|
137 |
end; |