# HG changeset patch
# User wenzelm
# Date 1726563603 -7200
# Node ID 59c91b2380344eccb00bf7907462c32845c8a40e
# Parent  5a75dc44623ad5371496e4c8092b189015a40a2e
tuned comments;

diff -r 5a75dc44623a -r 59c91b238034 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 17 10:47:08 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 17 11:00:03 2024 +0200
@@ -1,21 +1,25 @@
 (*  Title:      Pure/General/pretty.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Markus Wenzel, TU Munich
-
-Generic pretty printing module.
+    Author:     Makarius
 
-Loosely based on
-  D. C. Oppen, "Pretty Printing",
-  ACM Transactions on Programming Languages and Systems (1980), 465-483.
+Generic pretty printing.
 
-The object to be printed is given as a tree with indentation and line
-breaking information.  A "break" inserts a newline if the text until
-the next break is too long to fit on the current line.  After the newline,
-text is indented to the level of the enclosing block.  Normally, if a block
-is broken then all enclosing blocks will also be broken.
+The object to be printed is given as a tree with blocks and breaks. A block
+causes alignment and may specify additional indentation and markup. A break
+inserts a newline if the text until the next break is too long to fit on the
+current line. After the newline, text is indented to the level of the
+enclosing block. Normally, if a block is broken then all enclosing blocks will
+also be broken.
 
-The stored length of a block is used in break_dist (to treat each inner block as
-a unit for breaking).
+References:
+
+  * L. C. Paulson, "ML for the Working Programmer" (1996),
+    2nd edition, Cambridge University Press.
+    Section 8.10 "A pretty printer"
+    https://www.cl.cam.ac.uk/~lp15/MLbook/PDF/chapter8.pdf
+
+  * D. C. Oppen, "Pretty Printing",
+    ACM Transactions on Programming Languages and Systems (1980), 465-483.
 *)
 
 signature PRETTY =