equal
deleted
inserted
replaced
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_strings strs = |
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 app (fn s => TextIO.output (tmp_file, s)) strs; |
73 in |
74 TextIO.closeOut tmp_file; |
74 TextIO.output (tmp_file, txt); |
75 use tmp_name; |
75 TextIO.closeOut tmp_file; |
76 OS.FileSys.remove tmp_name |
76 use tmp_name; |
|
77 OS.FileSys.remove tmp_name |
77 end; |
78 end; |
78 |
79 |
79 |
80 |
80 |
81 |
81 (** OS related **) |
82 (** OS related **) |