src/Pure/General/source.ML
changeset 40627 becf5d5187cc
parent 38253 3d4e521014f7
child 54387 890e983cb07b
     1.1 --- a/src/Pure/General/source.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/General/source.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4  
     1.5  (* string source *)
     1.6  
     1.7 -val of_string = of_list o explode;
     1.8 +val of_string = of_list o raw_explode;
     1.9  
    1.10  fun of_string_limited limit str =
    1.11    make_source [] (Substring.full str) default_prompt
    1.12 @@ -127,14 +127,14 @@
    1.13          NONE => []
    1.14        | SOME 0 => []
    1.15        | SOME _ => TextIO.input instream :: slurp ());
    1.16 -  in maps explode (slurp ()) end;
    1.17 +  in maps raw_explode (slurp ()) end;
    1.18  
    1.19  fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
    1.20    let val input = slurp_input in_stream in
    1.21      if exists (fn c => c = "\n") input then (input, ())
    1.22      else
    1.23        (case (Output.prompt prompt; TextIO.inputLine in_stream) of
    1.24 -        SOME line => (input @ explode line, ())
    1.25 +        SOME line => (input @ raw_explode line, ())
    1.26        | NONE => (input, ()))
    1.27    end);
    1.28