margin 76 (2nd try :-);
authorwenzelm
Mon, 29 Sep 1997 15:08:47 +0200
changeset 3741 daa5ac720678
parent 3740 26992736d471
child 3742 6fccb16a7e3a
margin 76 (2nd try :-);
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;