author | wenzelm |
Mon, 29 Sep 1997 14:10:52 +0200 | |
changeset 3738 | 27f7473d029a |
parent 3737 | 3ea2f3b5e705 |
child 3739 | 13f7107676a0 |
--- 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*)