--- 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;