302 general template format is a sequence over any of the following |
302 general template format is a sequence over any of the following |
303 entities. |
303 entities. |
304 |
304 |
305 \begin{itemize} |
305 \begin{itemize} |
306 |
306 |
307 \item @{text "\<^bold>d"} is a delimiter, namely a non-empty |
307 \item @{text "d"} is a delimiter, namely a non-empty sequence of |
308 sequence of characters other than the special characters @{text "'"} |
308 characters other than the following special characters: |
309 (single quote), @{text "_"} (underscore), @{text "\<index>"} (index |
309 |
310 symbol), @{text "/"} (slash), @{text "("} and @{text ")"} |
310 \smallskip |
311 (parentheses). |
311 \begin{tabular}{ll} |
312 |
312 @{verbatim "'"} & single quote \\ |
313 A single quote escapes the special meaning of these meta-characters, |
313 @{verbatim "_"} & underscore \\ |
314 producing a literal version of the following character, unless that |
314 @{text "\<index>"} & index symbol \\ |
315 is a blank. A single quote followed by a blank separates |
315 @{verbatim "("} & open parenthesis \\ |
316 delimiters, without affecting printing, but input tokens may have |
316 @{verbatim ")"} & close parenthesis \\ |
317 additional white space here. |
317 @{verbatim "/"} & slash \\ |
318 |
318 \end{tabular} |
319 \item @{text "_"} is an argument position, which stands for a |
319 \medskip |
|
320 |
|
321 \item @{verbatim "'"} escapes the special meaning of these |
|
322 meta-characters, producing a literal version of the following |
|
323 character, unless that is a blank. |
|
324 |
|
325 A single quote followed by a blank separates delimiters, without |
|
326 affecting printing, but input tokens may have additional white space |
|
327 here. |
|
328 |
|
329 \item @{verbatim "_"} is an argument position, which stands for a |
320 certain syntactic category in the underlying grammar. |
330 certain syntactic category in the underlying grammar. |
321 |
331 |
322 \item @{text "\<index>"} is an indexed argument position; this is |
332 \item @{text "\<index>"} is an indexed argument position; this is the place |
323 the place where implicit structure arguments can be attached. |
333 where implicit structure arguments can be attached. |
324 |
334 |
325 \item @{text "\<^bold>s"} is a non-empty sequence of spaces for |
335 \item @{text "s"} is a non-empty sequence of spaces for printing. |
326 printing. This and the following specifications do not affect |
336 This and the following specifications do not affect parsing at all. |
327 parsing at all. |
337 |
328 |
338 \item @{verbatim "("}@{text n} opens a pretty printing block. The |
329 \item @{text "(\<^bold>n"} opens a pretty printing block. The |
|
330 optional number specifies how much indentation to add when a line |
339 optional number specifies how much indentation to add when a line |
331 break occurs within the block. If the parenthesis is not followed |
340 break occurs within the block. If the parenthesis is not followed |
332 by digits, the indentation defaults to 0. A block specified via |
341 by digits, the indentation defaults to 0. A block specified via |
333 @{text "(00"} is unbreakable. |
342 @{verbatim "(00"} is unbreakable. |
334 |
343 |
335 \item @{text ")"} closes a pretty printing block. |
344 \item @{verbatim ")"} closes a pretty printing block. |
336 |
345 |
337 \item @{text "//"} forces a line break. |
346 \item @{verbatim "//"} forces a line break. |
338 |
347 |
339 \item @{text "/\<^bold>s"} allows a line break. Here @{text |
348 \item @{verbatim "/"}@{text s} allows a line break. Here @{text s} |
340 "\<^bold>s"} stands for the string of spaces (zero or more) right |
349 stands for the string of spaces (zero or more) right after the |
341 after the slash. These spaces are printed if the break is |
350 slash. These spaces are printed if the break is \emph{not} taken. |
342 \emph{not} taken. |
|
343 |
351 |
344 \end{itemize} |
352 \end{itemize} |
345 |
353 |
346 For example, the template @{text "(_ +/ _)"} specifies an infix |
354 For example, the template @{verbatim "(_ +/ _)"} specifies an infix |
347 operator. There are two argument positions; the delimiter @{text |
355 operator. There are two argument positions; the delimiter |
348 "+"} is preceded by a space and followed by a space or line break; |
356 @{verbatim "+"} is preceded by a space and followed by a space or |
349 the entire phrase is a pretty printing block. |
357 line break; the entire phrase is a pretty printing block. |
350 |
358 |
351 The general idea of pretty printing with blocks and breaks is also |
359 The general idea of pretty printing with blocks and breaks is also |
352 described in \cite{paulson-ml2}. |
360 described in \cite{paulson-ml2}. |
353 *} |
361 *} |
354 |
362 |