145 ML{*val strip_specials = |
145 ML{*val strip_specials = |
146 let |
146 let |
147 fun strip ("\^A" :: _ :: cs) = strip cs |
147 fun strip ("\^A" :: _ :: cs) = strip cs |
148 | strip (c :: cs) = c :: strip cs |
148 | strip (c :: cs) = c :: strip cs |
149 | strip [] = []; |
149 | strip [] = []; |
150 in implode o strip o explode end; |
150 in |
|
151 implode o strip o explode |
|
152 end |
151 |
153 |
152 fun redirect_tracing stream = |
154 fun redirect_tracing stream = |
153 Output.tracing_fn := (fn s => |
155 Output.tracing_fn := (fn s => |
154 (TextIO.output (stream, (strip_specials s)); |
156 (TextIO.output (stream, (strip_specials s)); |
155 TextIO.output (stream, "\n"); |
157 TextIO.output (stream, "\n"); |
266 |
268 |
267 fun string_of_thms_no_vars ctxt thms = |
269 fun string_of_thms_no_vars ctxt thms = |
268 commas (map (string_of_thm_no_vars ctxt) thms) *} |
270 commas (map (string_of_thm_no_vars ctxt) thms) *} |
269 |
271 |
270 text {* |
272 text {* |
271 When printing out several `parcels' of information that belong |
273 When printing out several parcels of information that semantiaclly |
272 together you should try to keep this information together. For |
274 belong together, like a warning message consisting of a term and |
273 this you can use the function @{ML [index] cat_lines}, which |
275 a type, you should try to keep this information together |
|
276 in a single string. So do not print out information as |
|
277 |
|
278 @{ML_response_fake [display,gray] |
|
279 "tracing \"First half,\"; |
|
280 tracing \"and second half.\"" |
|
281 "First half, |
|
282 and second half."} |
|
283 |
|
284 but as a single string with appropriate formatting. For example |
|
285 |
|
286 @{ML_response_fake [display,gray] |
|
287 "tracing (\"First half,\" ^ \"\\n\" ^ \"and second half.\")" |
|
288 "First half, |
|
289 and second half."} |
|
290 |
|
291 To ease this kind of string manipulations, there are a number |
|
292 of library functions. For example, the function @{ML [index] cat_lines} |
274 concatenates a list of strings and inserts newlines. |
293 concatenates a list of strings and inserts newlines. |
275 |
294 |
276 @{ML_response [display, gray] |
295 @{ML_response [display, gray] |
277 "cat_lines [\"foo\", \"bar\"]" |
296 "cat_lines [\"foo\", \"bar\"]" |
278 "\"foo\\nbar\""} |
297 "\"foo\\nbar\""} |
|
298 |
|
299 Section \ref{sec:pretty} will also explain infrastructure that helps |
|
300 with more elaborate pretty printing. |
279 *} |
301 *} |
280 |
302 |
281 |
303 |
282 section {* Combinators\label{sec:combinators} *} |
304 section {* Combinators\label{sec:combinators} *} |
283 |
305 |