# HG changeset patch
# User wenzelm
# Date 1184705320 -7200
# Node ID c6094fe98dfd03a1d2b96508caaacf4a7a5cb620
# Parent  1990e9acc7d1e70cda783b29d533d234c686a274
adapted TextIO.inputLine;

diff -r 1990e9acc7d1 -r c6094fe98dfd src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Jul 17 22:48:39 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Jul 17 22:48:40 2007 +0200
@@ -13,7 +13,7 @@
 > use "ML-Systems/mosml.ML";
 > use "ROOT.ML";
 > Session.finish ();
-> cd "../HOL";
+> cd "../FOL";
 > use "ROOT.ML";
 *)
 
@@ -123,6 +123,9 @@
 struct
   fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
   open TextIO;
+  fun inputLine is =
+    let val s = TextIO.inputLine is
+    in if s = "" then NONE else SOME s end;
 end;