adapted TextIO.inputLine;

--- 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;