changeset 3738 | 27f7473d029a |
parent 2695 | 871b69a4b78f |
child 3741 | daa5ac720678 |
--- a/src/Pure/Syntax/pretty.ML Mon Sep 29 12:13:43 1997 +0200 +++ b/src/Pure/Syntax/pretty.ML Mon Sep 29 14:10:52 1997 +0200 @@ -96,7 +96,7 @@ (*** Formatting ***) -val margin = ref 80 (*right margin, or page width*) +val margin = ref 76 (*right margin, or page width*) and breakgain = ref 4 (*minimum added space required of a break*) and emergencypos = ref 40; (*position too far to right*)