| author | haftmann |
| Fri, 16 Dec 2005 15:52:05 +0100 | |
| changeset 18421 | 464c93701351 |
| parent 18160 | fb93c63c62f1 |
| child 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 |
Author: Makarius |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
4 |
|
| 18160 | 5 |
Turn the official PolyML 4.2.0 into the internal version 4.1.4, in |
6 |
order to make it work with Isabelle2005. This is to be commited into |
|
7 |
ML_dbase! *) |
|
|
17753
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
8 |
|
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
9 |
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
|
10 |
struct |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
11 |
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
|
12 |
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
|
13 |
struct |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
14 |
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
|
15 |
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
|
16 |
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
|
17 |
end; |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
18 |
end; |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
19 |
|
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
20 |
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
|
21 |
struct |
|
f84b032417ac
Patch for PolyML 4.1.4 to make it work with Isabelle2005. We commit this into ML_dbase!
wenzelm
parents:
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
end; |
| 17757 | 25 |
|
26 |
structure Substring = |
|
27 |
struct |
|
28 |
open Substring; |
|
29 |
val all = full; |
|
30 |
end; |