src/Pure/ML-Systems/polyml-5.1.ML
changeset 24600 5877b88f262c
parent 24584 01e83ffa6c54
child 24852 30da58e0a483
     1.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Sun Sep 16 14:52:34 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sun Sep 16 14:55:48 2007 +0200
     1.3 @@ -12,9 +12,9 @@
     1.4  
     1.5  (* improved versions of use_text/file *)
     1.6  
     1.7 -fun use_text name (print, err) verbose txt =
     1.8 +fun use_text (tune: string -> string) name (print, err) verbose txt =
     1.9    let
    1.10 -    val in_buffer = ref (explode txt);
    1.11 +    val in_buffer = ref (explode (tune txt));
    1.12      val out_buffer = ref ([]: string list);
    1.13      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.14  
    1.15 @@ -35,8 +35,8 @@
    1.16      if verbose then print (output ()) else ()
    1.17    end;
    1.18  
    1.19 -fun use_file output verbose name =
    1.20 +fun use_file tune output verbose name =
    1.21    let
    1.22      val instream = TextIO.openIn name;
    1.23      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.24 -  in use_text name output verbose txt end;
    1.25 +  in use_text tune name output verbose txt end;