| author | haftmann |
| Mon, 02 Oct 2006 23:00:51 +0200 | |
| changeset 20835 | 27d049062b56 |
| parent 17514 | 1d7771a659f6 |
| permissions | -rw-r--r-- |
|
14519
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/smlnj-basis-compat.ML |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
3 |
Author: Sebastian Skalberg (TU Muenchen) |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
4 |
|
| 14656 | 5 |
Compatibility file for Standard ML of New Jersey 110.44 or later. Here |
|
14519
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
6 |
signatures that have changed to adhere to the SML Basis Library are |
|
17514
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
7 |
changed back to their old values. |
|
14519
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
8 |
*) |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
9 |
|
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
10 |
structure TextIO = |
|
4ca3608fdf4f
Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents:
diff
changeset
|
11 |
struct |
|
17514
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
12 |
open TextIO; |
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
13 |
|
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
14 |
fun inputLine is = |
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
15 |
(case TextIO.inputLine is of |
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
16 |
SOME str => str |
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
17 |
| NONE => "") |
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
18 |
handle IO.Io _ => raise Interrupt; |
|
1d7771a659f6
TextIO.inputLine: handle IO.Io, assuming it stems from a signal;
wenzelm
parents:
14656
diff
changeset
|
19 |
end; |