author | paulson |
Fri, 05 Oct 2007 09:59:03 +0200 | |
changeset 24854 | 0ebcd575d3c6 |
parent 24852 | 30da58e0a483 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Pure/ML-Systems/polyml-5.1.ML |
23943 | 2 |
ID: $Id$ |
3 |
||
4 |
Compatibility wrapper for Poly/ML 5.1. |
|
5 |
*) |
|
6 |
||
7 |
use "ML-Systems/polyml.ML"; |
|
23966
25f34ff5eedf
moved exception capture/release to structure Exn;
wenzelm
parents:
23947
diff
changeset
|
8 |
use "ML-Systems/multithreading_polyml.ML"; |
23943 | 9 |
|
10 |
val pointer_eq = PolyML.pointerEq; |
|
11 |
||
12 |
||
24852 | 13 |
(* single-threaded profiling *) |
14 |
||
15 |
local val profile_orig = profile in |
|
16 |
||
17 |
fun profile 0 f x = f x |
|
18 |
| profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x); |
|
19 |
||
20 |
end; |
|
21 |
||
22 |
||
23943 | 23 |
(* improved versions of use_text/file *) |
24 |
||
24600
5877b88f262c
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24584
diff
changeset
|
25 |
fun use_text (tune: string -> string) name (print, err) verbose txt = |
23943 | 26 |
let |
24600
5877b88f262c
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24584
diff
changeset
|
27 |
val in_buffer = ref (explode (tune txt)); |
23943 | 28 |
val out_buffer = ref ([]: string list); |
29 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
|
30 |
||
31 |
val line_no = ref 1; |
|
32 |
fun line () = ! line_no; |
|
33 |
fun get () = |
|
34 |
(case ! in_buffer of |
|
35 |
[] => "" |
|
36 |
| c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); |
|
37 |
fun put s = out_buffer := s :: ! out_buffer; |
|
38 |
||
39 |
fun exec () = |
|
40 |
(case ! in_buffer of |
|
41 |
[] => () |
|
42 |
| _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); |
|
43 |
in |
|
44 |
exec () handle exn => (err (output ()); raise exn); |
|
45 |
if verbose then print (output ()) else () |
|
46 |
end; |
|
47 |
||
24600
5877b88f262c
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24584
diff
changeset
|
48 |
fun use_file tune output verbose name = |
23943 | 49 |
let |
50 |
val instream = TextIO.openIn name; |
|
51 |
val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
|
24600
5877b88f262c
use_text/file: tune text (cf. ML_Parse.fix_ints);
wenzelm
parents:
24584
diff
changeset
|
52 |
in use_text tune name output verbose txt end; |