| 21688 |      1 | (*  Title:      Pure/ML-Systems/polyml-5.0.ML
 | 
|  |      2 |     ID:         $Id$
 | 
|  |      3 | 
 | 
|  |      4 | Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
 | 
|  |      5 | *)
 | 
|  |      6 | 
 | 
|  |      7 | structure Posix =
 | 
|  |      8 | struct
 | 
|  |      9 |   open Posix;
 | 
|  |     10 |   structure IO =
 | 
|  |     11 |   struct
 | 
|  |     12 |     open IO;
 | 
|  |     13 |     val mkReader = mkTextReader;
 | 
|  |     14 |     val mkWriter = mkTextWriter;
 | 
|  |     15 |   end;
 | 
|  |     16 | end;
 | 
|  |     17 | 
 | 
|  |     18 | structure TextIO =
 | 
|  |     19 | struct
 | 
|  |     20 |   open TextIO;
 | 
|  |     21 |   fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
 | 
|  |     22 | end;
 | 
|  |     23 | 
 | 
|  |     24 | structure Substring =
 | 
|  |     25 | struct
 | 
|  |     26 |   open Substring;
 | 
|  |     27 |   val all = full;
 | 
|  |     28 | end;
 | 
|  |     29 | 
 | 
|  |     30 | 
 | 
|  |     31 | use "ML-Systems/polyml.ML";
 | 
|  |     32 | 
 | 
|  |     33 | val pointer_eq = PolyML.pointerEq;
 |