src/Pure/ML-Systems/polyml_old_basis.ML
author wenzelm
Fri, 03 Oct 2008 21:06:38 +0200
changeset 28490 40c3f900c457
parent 26216 c7d0cd2c7715
child 29564 f8b933a62151
permissions -rw-r--r--
removed obsolete Posix/Signal compatibility wrappers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26216
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml_old_basis.ML
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     3
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     4
Fixes for the old SML basis library (before Poly/ML 4.2.0).
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     5
*)
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     6
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     7
structure String =
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     8
struct
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
     9
  fun isSuffix s1 s2 =
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    10
    let val n1 = size s1 and n2 = size s2
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    11
    in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    12
  fun isSubstring s1 s2 =
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    13
    String.isPrefix s1 s2 orelse
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    14
      size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    15
  open String;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    16
end;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    17
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    18
structure Substring =
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    19
struct
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    20
  open Substring;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    21
  val full = all;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    22
end;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    23
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    24
structure TextIO =
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    25
struct
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    26
  open TextIO;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    27
  fun inputLine is =
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    28
    let val s = TextIO.inputLine is
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    29
    in if s = "" then NONE else SOME s end;
c7d0cd2c7715 renamed polyml-old-basis.ML to polyml_old_basis.ML;
wenzelm
parents:
diff changeset
    30
end;