author | wenzelm |
Thu, 06 Mar 2008 19:21:26 +0100 | |
changeset 26215 | 94d32a7cd0fb |
parent 26084 | a7475459c740 |
child 26379 | a01a05cdd3b8 |
permissions | -rw-r--r-- |
2341 | 1 |
(* Title: Pure/ML-Systems/polyml.ML |
2 |
ID: $Id$ |
|
3 |
||
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
4 |
Compatibility wrapper for Poly/ML 5.1/5.2. |
2341 | 5 |
*) |
6 |
||
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
7 |
use "ML-Systems/polyml_common.ML"; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
8 |
use "ML-Systems/multithreading_polyml.ML"; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
9 |
|
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
10 |
val pointer_eq = PolyML.pointerEq; |
23921
947152add153
added compatibility file for ML systems without multithreading;
wenzelm
parents:
23826
diff
changeset
|
11 |
|
25023 | 12 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
13 |
(* single-threaded profiling *) |
24598 | 14 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
15 |
local val profile_orig = profile in |
17077 | 16 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
17 |
fun profile 0 f x = f x |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
18 |
| profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x); |
2341 | 19 |
|
7148 | 20 |
end; |
6042 | 21 |
|
2341 | 22 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
23 |
(* improved versions of use_text/file *) |
3588 | 24 |
|
24598 | 25 |
fun use_text (tune: string -> string) name (print, err) verbose txt = |
3588 | 26 |
let |
24598 | 27 |
val in_buffer = ref (explode (tune txt)); |
5090 | 28 |
val out_buffer = ref ([]: string list); |
21715 | 29 |
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs)); |
5090 | 30 |
|
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
31 |
val line_no = ref 1; |
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
32 |
fun line () = ! line_no; |
5038 | 33 |
fun get () = |
5090 | 34 |
(case ! in_buffer of |
5038 | 35 |
[] => "" |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
36 |
| c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c)); |
5090 | 37 |
fun put s = out_buffer := s :: ! out_buffer; |
38 |
||
5038 | 39 |
fun exec () = |
5090 | 40 |
(case ! in_buffer of |
5038 | 41 |
[] => () |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
42 |
| _ => (PolyML.compilerEx (get, put, line, name) (); exec ())); |
5090 | 43 |
in |
26215
94d32a7cd0fb
rearrangements to make latest Poly/ML the default, not old 4.x;
wenzelm
parents:
26084
diff
changeset
|
44 |
exec () handle exn => (err (output ()); raise exn); |
10914 | 45 |
if verbose then print (output ()) else () |
5090 | 46 |
end; |
3588 | 47 |
|
24598 | 48 |
fun use_file tune output verbose name = |
49 |
let |
|
50 |
val instream = TextIO.openIn name; |
|
51 |
val txt = TextIO.inputAll instream before TextIO.closeIn instream; |
|
52 |
in use_text tune name output verbose txt end; |