src/Pure/ML-Systems/polyml-old-basis.ML
author wenzelm
Tue, 24 Jul 2007 19:44:33 +0200
changeset 23962 e0358fac0541
parent 23141 1f6b6a7314cf
child 24564 260a65fa2900
permissions -rw-r--r--
Runtime exceptions as values (from library.ML);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23139
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-old-basis.ML
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     3
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     4
Fixes for the old SML basis library (before Poly/ML 4.2.0).
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     5
*)
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     6
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     7
structure String =
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     8
struct
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
     9
  fun isSuffix s1 s2 =
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    10
    let val n1 = size s1 and n2 = size s2
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    11
    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
23141
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    12
  open String;
23139
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    13
end;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    14
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    15
structure Substring =
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    16
struct
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    17
  open Substring;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    18
  val full = all;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    19
end;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    20
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    21
structure Posix =
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    22
struct
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    23
  open Posix;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    24
  structure IO =
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    25
  struct
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    26
    open IO;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    27
    val mkTextReader = mkReader;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    28
    val mkTextWriter = mkWriter;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    29
  end;
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents:
diff changeset
    30
end;
23141
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    31
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    32
structure TextIO =
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    33
struct
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    34
  open TextIO;
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    35
  fun inputLine is =
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    36
    let val s = TextIO.inputLine is
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    37
    in if s = "" then NONE else SOME s end;
1f6b6a7314cf emulate later version of TextIO.inputLine;
wenzelm
parents: 23139
diff changeset
    38
end;