src/Pure/ML-Systems/mlworks.ML
changeset 5090 75ac9b451ae0
parent 5038 301c37df931d
child 5660 f2c5354cd32f
equal deleted inserted replaced
5089:f95e0a6eb775 5090:75ac9b451ae0
    64 
    64 
    65 
    65 
    66 (* ML command execution *)
    66 (* ML command execution *)
    67 
    67 
    68 (*Can one redirect 'use' directly to an instream?*)
    68 (*Can one redirect 'use' directly to an instream?*)
    69 fun use_text txt =
    69 fun use_text _ txt =
    70   let
    70   let
    71     val tmp_name = OS.FileSys.tmpName ();
    71     val tmp_name = OS.FileSys.tmpName ();
    72     val tmp_file = TextIO.openOut tmp_name;
    72     val tmp_file = TextIO.openOut tmp_name;
    73   in
    73   in
    74     TextIO.output (tmp_file, txt);
    74     TextIO.output (tmp_file, txt);