| author | wenzelm | 
| Sat, 19 Nov 2005 14:21:05 +0100 | |
| changeset 18208 | dbdcf366db53 | 
| 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; |