author | wenzelm |
Wed, 29 Nov 2006 15:44:59 +0100 | |
changeset 21592 | 8831206d7f41 |
parent 21299 | 4b01726d71fc |
permissions | -rw-r--r-- |
17753
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml-4.1.4-patch.ML |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
3 |
|
21299 | 4 |
Basis library fixes for Poly/ML 4.2.0 or later. |
5 |
*) |
|
17753
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
6 |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
7 |
structure Posix = |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
8 |
struct |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
9 |
open Posix; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
10 |
structure IO = |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
11 |
struct |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
12 |
open IO; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
13 |
val mkReader = mkTextReader; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
14 |
val mkWriter = mkTextWriter; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
15 |
end; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
16 |
end; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
17 |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
18 |
structure TextIO = |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
19 |
struct |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
20 |
open TextIO; |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
21 |
fun inputLine is = Option.getOpt (TextIO.inputLine is, ""); |
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
22 |
end; |
17757 | 23 |
|
24 |
structure Substring = |
|
25 |
struct |
|
26 |
open Substring; |
|
27 |
val all = full; |
|
28 |
end; |