src/Pure/ML-Systems/polyml-4.1.4-patch.ML
author wenzelm
Mon, 14 Nov 2005 14:36:29 +0100
changeset 18160 fb93c63c62f1
parent 17757 87a9b1d48e25
child 21299 4b01726d71fc
permissions -rw-r--r--
tuned;
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
    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
wenzelm
parents: 17757
diff changeset
     5
Turn the official PolyML 4.2.0 into the internal version 4.1.4, in
wenzelm
parents: 17757
diff changeset
     6
order to make it work with Isabelle2005.  This is to be commited into
wenzelm
parents: 17757
diff changeset
     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
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    25
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    26
structure Substring =
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    27
struct
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    28
  open Substring;
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    29
  val all = full;
87a9b1d48e25 Substring.all = Substring.full;
wenzelm
parents: 17753
diff changeset
    30
end;