author | wenzelm |
Mon, 14 Nov 2005 14:36:29 +0100 | |
changeset 18160 | fb93c63c62f1 |
parent 17757 | 87a9b1d48e25 |
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; |