equal
deleted
inserted
replaced
360 \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following |
360 \<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following |
361 specifications do not affect parsing at all. |
361 specifications do not affect parsing at all. |
362 |
362 |
363 \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how |
363 \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how |
364 much indentation to add when a line break occurs within the block. If the |
364 much indentation to add when a line break occurs within the block. If the |
365 parenthesis is not followed by digits, the indentation defaults to 0. A |
365 parenthesis is not followed by digits, the indentation defaults to 0. |
366 block specified via \<^verbatim>\<open>(00\<close> is unbreakable. |
|
367 |
366 |
368 \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block. |
367 \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block. |
369 |
368 |
370 \<^descr> \<^verbatim>\<open>//\<close> forces a line break. |
369 \<^descr> \<^verbatim>\<open>//\<close> forces a line break. |
371 |
370 |