author | wenzelm |
Thu, 24 Apr 1997 19:46:24 +0200 | |
changeset 3048 | a4b609108712 |
parent 2425 | 4db9e4a150d6 |
child 3591 | 412c62dd43de |
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 |
|
3048 | 6 |
Compatibility file for Standard ML of New Jersey, version 1.09.27 or later. |
2342
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 |
|
3048 | 9 |
(** Poly/ML emulation **) |
2342
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 |
|
3048 | 13 |
(*to limit the printing depth [divided by 2 for comparibility with Poly/ML]*) |
14 |
fun print_depth n = |
|
15 |
(Compiler.Control.Print.printDepth := n div 2; |
|
16 |
Compiler.Control.Print.printLength := n); |
|
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
17 |
|
2425 | 18 |
Compiler.Control.primaryPrompt := "> "; |
19 |
Compiler.Control.secondaryPrompt := "# "; |
|
20 |
||
21 |
||
3048 | 22 |
(* interface for toplevel pretty printers, see also Pure/install_pp.ML *) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
23 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
24 |
fun make_pp path pprint = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
25 |
let |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
26 |
open Compiler.PrettyPrint; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
27 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
28 |
fun pp pps obj = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
29 |
pprint obj |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
30 |
(add_string pps, begin_block pps INCONSISTENT, |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
31 |
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
|
32 |
fn () => end_block pps); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
33 |
in |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
34 |
(path, pp) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
35 |
end; |
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 |
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
|
38 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
39 |
|
3048 | 40 |
(** New Jersey ML parameters **) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
41 |
|
3048 | 42 |
val _ = |
43 |
(Compiler.Control.Print.printLength := 1000; |
|
44 |
Compiler.Control.Print.printDepth := 350; |
|
45 |
Compiler.Control.Print.stringDepth := 250; |
|
46 |
Compiler.Control.Print.signatures := 2); |
|
2342
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 |
|
3048 | 49 |
(** Character / string functions which are compatible with 0.93 and Poly/ML **) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
50 |
|
3048 | 51 |
fun ord s = Char.ord (String.sub (s, 0)); |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
52 |
val chr = str o Char.chr; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
53 |
val explode = (map str) o String.explode; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
54 |
val implode = String.concat; |
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 |
|
3048 | 57 |
(** Timing functions **) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
58 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
59 |
(*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
|
60 |
prints its runtime. *) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
61 |
fun cond_timeit flag f = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
62 |
if flag then |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
63 |
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
|
64 |
val CPUtimer = Timer.startCPUTimer(); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
65 |
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
|
66 |
val result = f(); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
67 |
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
|
68 |
in print("User " ^ toString (usrt2-usrt1) ^ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
69 |
" GC " ^ toString (gct2-gct1) ^ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
70 |
" All "^ toString (syst2-syst1 + usrt2-usrt1 + gct2-gct1) ^ |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
71 |
" secs\n") |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
72 |
handle Time => (); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
73 |
result |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
74 |
end |
3048 | 75 |
else f (); |
2342
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 |
|
3048 | 78 |
(** File handling **) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
79 |
|
3048 | 80 |
(*get time of last modification; if file doesn't exist return an empty string*) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
81 |
fun file_info "" = "" |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
82 |
| 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
|
83 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
84 |
|
3048 | 85 |
(** ML command execution **) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
86 |
|
3048 | 87 |
val use_string = Compiler.Interact.useStream o TextIO.openString o implode; |
2342
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 |
|
3048 | 90 |
(** System command execution **) |
2342
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
91 |
|
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
92 |
(*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
|
93 |
sends its output to stdout. |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
94 |
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
|
95 |
doesn't use the PATH.*) |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
96 |
fun execute command = |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
97 |
let val tmp_name = "isa_converted.tmp" |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
98 |
val is = (OS.Process.system (command ^ " > " ^ tmp_name); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
99 |
TextIO.openIn tmp_name); |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
100 |
val result = TextIO.inputAll is; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
101 |
in TextIO.closeIn is; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
102 |
OS.FileSys.remove tmp_name; |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
103 |
result |
859d72636ce7
Compatibility file for Standard ML of New Jersey, version 1.09.
wenzelm
parents:
diff
changeset
|
104 |
end; |
2408 | 105 |
|
106 |
||
3048 | 107 |
(** non-ASCII input **) |
2408 | 108 |
|
109 |
val needs_filtered_use = false; |