src/Pure/General/pretty.ML
changeset 6321 207f518167e8
parent 6271 957d8aa4a06b
child 8456 8ccda76f07cb
     1.1 --- a/src/Pure/General/pretty.ML	Tue Mar 09 12:10:13 1999 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Mar 09 12:11:00 1999 +0100
     1.3 @@ -28,6 +28,7 @@
     1.4    type T
     1.5    val str: string -> T
     1.6    val strlen: string -> int -> T
     1.7 +  val strlen_real: string -> real -> T
     1.8    val sym: string -> T
     1.9    val spc: int -> T
    1.10    val brk: int -> T
    1.11 @@ -50,6 +51,7 @@
    1.12    val pprint: T -> pprint_args -> unit
    1.13    val setdepth: int -> unit
    1.14    val setmargin: int -> unit
    1.15 +  val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    1.16    end;
    1.17  
    1.18  structure Pretty : PRETTY =
    1.19 @@ -100,18 +102,14 @@
    1.20  
    1.21  (* margin *)
    1.22  
    1.23 -(*example values*)
    1.24 -val margin      = ref 80        (*right margin, or page width*)
    1.25 -and breakgain   = ref 4         (*minimum added space required of a break*)
    1.26 -and emergencypos = ref 40;      (*position too far to right*)
    1.27 +fun make_margin_info m =
    1.28 + {margin = m,                   (*right margin, or page width*)
    1.29 +  breakgain = m div 20,         (*minimum added space required of a break*)
    1.30 +  emergencypos = m div 2};      (*position too far to right*)
    1.31  
    1.32 -fun setmargin m =
    1.33 -    (margin     := m;
    1.34 -     breakgain  := !margin div 20;
    1.35 -     emergencypos := !margin div 2);
    1.36 -
    1.37 -val () = setmargin 76;
    1.38 -
    1.39 +val margin_info = ref (make_margin_info 76);
    1.40 +fun setmargin m = margin_info := make_margin_info m;
    1.41 +fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
    1.42  
    1.43  (*Search for the next break (at this or higher levels) and force it to occur*)
    1.44  fun forcenext [] = []
    1.45 @@ -125,7 +123,7 @@
    1.46    | format (e::es, blockin, after) (text as {pos,nl,...}) =
    1.47      (case e of
    1.48         Block(bes,indent,wd) =>
    1.49 -         let val blockin' = (pos + indent) mod !emergencypos
    1.50 +         let val blockin' = (pos + indent) mod #emergencypos (! margin_info)
    1.51               val btext = format(bes, blockin', breakdist(es,after)) text
    1.52               (*If this block was broken then force the next break.*)
    1.53               val es2 = if nl < #nl(btext) then forcenext es else es
    1.54 @@ -135,8 +133,8 @@
    1.55                              or if breaking would add only breakgain to space *)
    1.56             format (es,blockin,after)
    1.57                 (if not force andalso
    1.58 -                   pos+wd <= Int.max(!margin - breakdist(es,after),
    1.59 -                                     blockin + !breakgain)
    1.60 +                   pos+wd <= Int.max(#margin (! margin_info) - breakdist(es,after),
    1.61 +                                     blockin + #breakgain (! margin_info))
    1.62                  then blanks wd text  (*just insert wd blanks*)
    1.63                  else blanks blockin (newline text)));
    1.64  
    1.65 @@ -149,6 +147,7 @@
    1.66  
    1.67  fun str s = String (s, size s);
    1.68  fun strlen s len = String (s, len);
    1.69 +fun strlen_real s len = strlen s (Real.round len);
    1.70  val sym = String o apsnd Real.round o Symbol.output_width;
    1.71  
    1.72  fun spc n = str (repstring " " n);
    1.73 @@ -216,7 +215,7 @@
    1.74  fun prune dp e = if dp>0 then pruning dp e else e;
    1.75  
    1.76  
    1.77 -fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
    1.78 +fun string_of e = #tx (format ([prune (! depth) e], 0, 0) emptytext);
    1.79  
    1.80  val writeln = writeln o string_of;
    1.81  
    1.82 @@ -228,9 +227,7 @@
    1.83        | s_of (String (s, _)) = s
    1.84        | s_of (Break (false, wd)) = repstring " " wd
    1.85        | s_of (Break (true, _)) = " ";
    1.86 -  in
    1.87 -    s_of (prune (! depth) prt)
    1.88 -  end;
    1.89 +  in s_of (prune (! depth) prt) end;
    1.90  
    1.91  (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
    1.92  fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =