# HG changeset patch
# User wenzelm
# Date 875538527 -7200
# Node ID daa5ac720678f72ababbbcd040b85a1ae3699d84
# Parent  26992736d4713599ff1e609a423f73eb0729467f
margin 76 (2nd try :-);

diff -r 26992736d471 -r daa5ac720678 src/Pure/Syntax/pretty.ML
--- a/src/Pure/Syntax/pretty.ML	Mon Sep 29 14:12:02 1997 +0200
+++ b/src/Pure/Syntax/pretty.ML	Mon Sep 29 15:08:47 1997 +0200
@@ -96,7 +96,10 @@
 
 (*** Formatting ***)
 
-val margin      = ref 76        (*right margin, or page width*)
+(* margin *)
+
+(*example values*)
+val margin      = ref 80        (*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*)
 
@@ -105,6 +108,9 @@
      breakgain  := !margin div 20;
      emergencypos := !margin div 2);
 
+val () = setmargin 76;
+
+
 (*Search for the next break (at this or higher levels) and force it to occur*)
 fun forcenext [] = []
   | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
@@ -235,8 +241,4 @@
   end;
 
 
-(*** Initialization ***)
-
-val () = setmargin 80;
-
 end;