src/Pure/ML-Systems/polyml-4.1.4-patch.ML
author wenzelm
Wed, 29 Nov 2006 15:44:59 +0100
changeset 21592 8831206d7f41
parent 21299 4b01726d71fc
permissions -rw-r--r--
renamed SIMPLE_METHOD' to SIMPLE_METHOD''; added simple version of SIMPLE_METHOD';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
4b01726d71fc tuned comments;
wenzelm
parents: 18160
diff changeset
     4
Basis library fixes for Poly/ML 4.2.0 or later.
4b01726d71fc tuned comments;
wenzelm
parents: 18160
diff changeset
     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
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    23
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    24
structure Substring =
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    25
struct
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    26
  open Substring;
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    27
  val all = full;
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    28
end;