src/Pure/ML-Systems/mosml.ML

 $ isabelle RAW_ML_SYSTEM
 > val ml_system = "mosml";
 > use "ML-Systems/mosml.ML";
 > use "ROOT.ML";
 > Session.finish ();
-> cd "../HOL";
+> cd "../FOL";
 > use "ROOT.ML";
 *)
 
 (** ML system related **)
 

 
 structure TextIO =
 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;
 
 
 (* bounded time execution *)