wenzelm@26216: (*  Title:      Pure/ML-Systems/polyml_old_basis.ML
wenzelm@26216: 
wenzelm@26216: Fixes for the old SML basis library (before Poly/ML 4.2.0).
wenzelm@26216: *)
wenzelm@26216: 
wenzelm@26216: structure String =
wenzelm@26216: struct
wenzelm@26216:   fun isSuffix s1 s2 =
wenzelm@26216:     let val n1 = size s1 and n2 = size s2
wenzelm@26216:     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
wenzelm@26216:   fun isSubstring s1 s2 =
wenzelm@26216:     String.isPrefix s1 s2 orelse
wenzelm@26216:       size s1 < size s2 andalso isSubstring s1 (String.extract (s2, 1, NONE)); 
wenzelm@26216:   open String;
wenzelm@26216: end;
wenzelm@26216: 
wenzelm@26216: structure Substring =
wenzelm@26216: struct
wenzelm@26216:   open Substring;
wenzelm@26216:   val full = all;
wenzelm@26216: end;
wenzelm@26216: 
wenzelm@26216: structure TextIO =
wenzelm@26216: struct
wenzelm@26216:   open TextIO;
wenzelm@26216:   fun inputLine is =
wenzelm@26216:     let val s = TextIO.inputLine is
wenzelm@26216:     in if s = "" then NONE else SOME s end;
wenzelm@26216: end;