equal
deleted
inserted
replaced
80 |
80 |
81 (** output channels **) |
81 (** output channels **) |
82 |
82 |
83 (* output primitives -- normally NOT used directly!*) |
83 (* output primitives -- normally NOT used directly!*) |
84 |
84 |
85 fun std_output s = CRITICAL (fn () => |
85 fun std_output s = NAMED_CRITICAL "IO" (fn () => |
86 (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut)); |
86 (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut)); |
87 |
87 |
88 fun std_error s = CRITICAL (fn () => |
88 fun std_error s = NAMED_CRITICAL "IO" (fn () => |
89 (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)); |
89 (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)); |
90 |
90 |
91 val immediate_output = std_output o output; |
91 val immediate_output = std_output o output; |
92 val writeln_default = std_output o suffix "\n"; |
92 val writeln_default = std_output o suffix "\n"; |
93 |
93 |