1.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Jun 15 11:05:25 1998 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Jun 15 11:06:00 1998 +0200
     1.3 @@ -41,22 +41,18 @@
     1.4  
     1.5  (* ML command execution -- 'eval' *)
     1.6  
     1.7 -val use_strings =
     1.8 +fun use_text txt =
     1.9    let
    1.10 -    fun exec line =
    1.11 -      let
    1.12 -        val is_first = ref true;
    1.13 -
    1.14 -        fun get_line () =
    1.15 -          if ! is_first then (is_first := false; line)
    1.16 -          else raise Io "use_strings: buffer exhausted";
    1.17 -      in
    1.18 -        PolyML.compiler (get_line, print) ()
    1.19 -      end;
    1.20 -
    1.21 -    fun execs [] = ()
    1.22 -      | execs (line :: lines) = (exec line; execs lines);
    1.23 -  in execs end;
    1.24 +    val buffer = ref (explode txt);
    1.25 +    fun get () =
    1.26 +      (case ! buffer of
    1.27 +        [] => ""
    1.28 +      | c :: cs => (buffer := cs; c));
    1.29 +    fun exec () =
    1.30 +      (case ! buffer of
    1.31 +        [] => ()
    1.32 +      | _ => (PolyML.compiler (get, print) (); exec ()));
    1.33 +  in exec () end;
    1.34  
    1.35  
    1.36