equal
deleted
inserted
replaced
172 in |
172 in |
173 implode o strip o explode |
173 implode o strip o explode |
174 end |
174 end |
175 |
175 |
176 fun redirect_tracing stream = |
176 fun redirect_tracing stream = |
177 Output.tracing_fn := (fn s => |
177 Output.Private_Hooks.tracing_fn := (fn s => |
178 (TextIO.output (stream, (strip_specials s)); |
178 (TextIO.output (stream, (strip_specials s)); |
179 TextIO.output (stream, "\n"); |
179 TextIO.output (stream, "\n"); |
180 TextIO.flushOut stream)) *} |
180 TextIO.flushOut stream)) *} |
181 |
181 |
182 text {* |
182 text {* |