src/Pure/ML-Systems/polyml-5.0.ML
changeset 24605 98689b0e5956
parent 24600 5877b88f262c
child 26215 94d32a7cd0fb
equal deleted inserted replaced
24604:d5c5d2e13fbf 24605:98689b0e5956
    32   in
    32   in
    33     exec () handle exn => (err (output ()); raise exn);
    33     exec () handle exn => (err (output ()); raise exn);
    34     if verbose then print (output ()) else ()
    34     if verbose then print (output ()) else ()
    35   end;
    35   end;
    36 
    36 
    37 fun use_file output verbose name =
    37 fun use_file tune output verbose name =
    38   let
    38   let
    39     val instream = TextIO.openIn name;
    39     val instream = TextIO.openIn name;
    40     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    40     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    41   in use_text name output verbose txt end;
    41   in use_text tune name output verbose txt end;