author | wenzelm |
Mon, 09 Dec 1996 16:33:57 +0100 | |
changeset 2342 | 859d72636ce7 |
child 2408 | acddf41dbbf7 |
permissions | -rw-r--r-- |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/smlnj-1.09.ML |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
3 |
Author: Carsten Clasohm, TU Muenchen |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
4 |
Copyright 1996 TU Muenchen |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
5 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
6 |
Compatibility file for Standard ML of New Jersey, version 1.09. |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
7 |
*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
8 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
9 |
(*** Poly/ML emulation ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
10 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
11 |
fun quit () = exit 0; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
12 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
13 |
(*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
14 |
fun print_depth n = (Compiler.Control.Print.printDepth := n div 2; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
15 |
Compiler.Control.Print.printLength := n); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
16 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
17 |
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
18 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
19 |
fun make_pp path pprint = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
20 |
let |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
21 |
open Compiler.PrettyPrint; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
22 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
23 |
fun pp pps obj = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
24 |
pprint obj |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
25 |
(add_string pps, begin_block pps INCONSISTENT, |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
26 |
fn wd => add_break pps (wd, 0), fn () => add_newline pps, |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
27 |
fn () => end_block pps); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
28 |
in |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
29 |
(path, pp) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
30 |
end; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
31 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
32 |
fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
33 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
34 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
35 |
(*** New Jersey ML parameters ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
36 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
37 |
(* Suppresses Garbage Collection messages; doesn't work yet *) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
38 |
(*System.Runtime.gc 0;*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
39 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
40 |
val _ = (Compiler.Control.Print.printLength := 1000; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
41 |
Compiler.Control.Print.printDepth := 350; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
42 |
Compiler.Control.Print.stringDepth := 250; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
43 |
Compiler.Control.Print.signatures := 2); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
44 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
45 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
46 |
(*** Character/string functions which are compatible with 0.93 and Poly/ML ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
47 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
48 |
fun ord s = Char.ord (String.sub(s,0)); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
49 |
val chr = str o Char.chr; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
50 |
val explode = (map str) o String.explode; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
51 |
val implode = String.concat; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
52 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
53 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
54 |
(*** Timing functions ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
55 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
56 |
(*A conditional timing function: applies f to () and, if the flag is true, |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
57 |
prints its runtime. *) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
58 |
fun cond_timeit flag f = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
59 |
if flag then |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
60 |
let open Time (*...for Time.toString, Time.+ and Time.- *) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
61 |
val CPUtimer = Timer.startCPUTimer(); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
62 |
val {gc=gct1,sys=syst1,usr=usrt1} = Timer.checkCPUTimer(CPUtimer); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
63 |
val result = f(); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
64 |
val {gc=gct2,sys=syst2,usr=usrt2} = Timer.checkCPUTimer(CPUtimer) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
65 |
in print("User " ^ toString (usrt2-usrt1) ^ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
66 |
" GC " ^ toString (gct2-gct1) ^ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
67 |
" All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
68 |
" secs\n") |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
69 |
handle Time => (); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
70 |
result |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
71 |
end |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
72 |
else f(); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
73 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
74 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
75 |
(*** File handling ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
76 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
77 |
(*Get time of last modification; if file doesn't exist return an empty string*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
78 |
fun file_info "" = "" |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
79 |
| file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>""; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
80 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
81 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
82 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
83 |
(*** ML command execution ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
84 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
85 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
86 |
(*For version 109.21 and later: |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
87 |
val use_string = Compiler.Interact.useStream o TextIO.openString o implode; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
88 |
*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
89 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
90 |
(*For versions prior to 109.21:*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
91 |
fun use_string commands = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
92 |
Compiler.Interact.use_stream (open_string (implode commands)); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
93 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
94 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
95 |
(*** System command execution ***) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
96 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
97 |
(*Execute an Unix command which doesn't take any input from stdin and |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
98 |
sends its output to stdout. |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
99 |
This could be done more easily by Unix.execute, but that function |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
100 |
doesn't use the PATH.*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
101 |
fun execute command = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
102 |
let val tmp_name = "isa_converted.tmp" |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
103 |
val is = (OS.Process.system (command ^ " > " ^ tmp_name); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
104 |
TextIO.openIn tmp_name); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
105 |
val result = TextIO.inputAll is; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
106 |
in TextIO.closeIn is; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
107 |
OS.FileSys.remove tmp_name; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
108 |
result |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
109 |
end; |