src/Pure/General/pretty.ML
author wenzelm
Tue Mar 09 12:11:00 1999 +0100 (1999-03-09)
changeset 6321 207f518167e8
parent 6271 957d8aa4a06b
child 8456 8ccda76f07cb
permissions -rw-r--r--
added strlen_real, setmp_margin;
     1 (*  Title:      Pure/General/pretty.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1991  University of Cambridge
     5 
     6 Generic pretty printing module.
     7 
     8 Loosely based on
     9   D. C. Oppen, "Pretty Printing",
    10   ACM Transactions on Programming Languages and Systems (1980), 465-483.
    11 
    12 The object to be printed is given as a tree with indentation and line
    13 breaking information.  A "break" inserts a newline if the text until
    14 the next break is too long to fit on the current line.  After the newline,
    15 text is indented to the level of the enclosing block.  Normally, if a block
    16 is broken then all enclosing blocks will also be broken.  Only "inconsistent
    17 breaks" are provided.
    18 
    19 The stored length of a block is used in breakdist (to treat each inner block as
    20 a unit for breaking).
    21 *)
    22 
    23 type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
    24   (unit -> unit) * (unit -> unit);
    25 
    26 signature PRETTY =
    27   sig
    28   type T
    29   val str: string -> T
    30   val strlen: string -> int -> T
    31   val strlen_real: string -> real -> T
    32   val sym: string -> T
    33   val spc: int -> T
    34   val brk: int -> T
    35   val fbrk: T
    36   val blk: int * T list -> T
    37   val lst: string * string -> T list -> T
    38   val quote: T -> T
    39   val commas: T list -> T list
    40   val breaks: T list -> T list
    41   val fbreaks: T list -> T list
    42   val block: T list -> T
    43   val strs: string list -> T
    44   val enclose: string -> string -> T list -> T
    45   val list: string -> string -> T list -> T
    46   val str_list: string -> string -> string list -> T
    47   val big_list: string -> T list -> T
    48   val string_of: T -> string
    49   val writeln: T -> unit
    50   val str_of: T -> string
    51   val pprint: T -> pprint_args -> unit
    52   val setdepth: int -> unit
    53   val setmargin: int -> unit
    54   val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    55   end;
    56 
    57 structure Pretty : PRETTY =
    58 struct
    59 
    60 (*printing items: compound phrases, strings, and breaks*)
    61 datatype T =
    62   Block of T list * int * int |         (*body, indentation, length*)
    63   String of string * int |              (*text, length*)
    64   Break of bool * int;                  (*mandatory flag, width if not taken*);
    65 
    66 (*Add the lengths of the expressions until the next Break; if no Break then
    67   include "after", to account for text following this block. *)
    68 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
    69   | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
    70   | breakdist (Break _ :: es, after) = 0
    71   | breakdist ([], after) = after;
    72 
    73 fun repstring a 0 = ""
    74   | repstring a 1 = a
    75   | repstring a k =
    76       if k mod 2 = 0 then repstring(a^a) (k div 2)
    77                      else repstring(a^a) (k div 2) ^ a;
    78 
    79 (*** Type for lines of text: string, # of lines, position on line ***)
    80 
    81 type text = {tx: string, nl: int, pos: int};
    82 
    83 val emptytext = {tx="", nl=0, pos=0};
    84 
    85 fun blanks wd {tx,nl,pos} =
    86     {tx  = tx ^ repstring " " wd,
    87      nl  = nl,
    88      pos = pos+wd};
    89 
    90 fun newline {tx,nl,pos} =
    91     {tx  = tx ^ "\n",
    92      nl  = nl+1,
    93      pos = 0};
    94 
    95 fun string s len {tx,nl,pos:int} =
    96     {tx  = tx ^ s,
    97      nl  = nl,
    98      pos = pos + len};
    99 
   100 
   101 (*** Formatting ***)
   102 
   103 (* margin *)
   104 
   105 fun make_margin_info m =
   106  {margin = m,                   (*right margin, or page width*)
   107   breakgain = m div 20,         (*minimum added space required of a break*)
   108   emergencypos = m div 2};      (*position too far to right*)
   109 
   110 val margin_info = ref (make_margin_info 76);
   111 fun setmargin m = margin_info := make_margin_info m;
   112 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
   113 
   114 (*Search for the next break (at this or higher levels) and force it to occur*)
   115 fun forcenext [] = []
   116   | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   117   | forcenext (e :: es) = e :: forcenext es;
   118 
   119 (*es is list of expressions to print;
   120   blockin is the indentation of the current block;
   121   after is the width of the following context until next break. *)
   122 fun format ([], _, _) text = text
   123   | format (e::es, blockin, after) (text as {pos,nl,...}) =
   124     (case e of
   125        Block(bes,indent,wd) =>
   126          let val blockin' = (pos + indent) mod #emergencypos (! margin_info)
   127              val btext = format(bes, blockin', breakdist(es,after)) text
   128              (*If this block was broken then force the next break.*)
   129              val es2 = if nl < #nl(btext) then forcenext es else es
   130          in  format (es2,blockin,after) btext  end
   131      | String (s, len) => format (es,blockin,after) (string s len text)
   132      | Break(force,wd) => (*no break if text to next break fits on this line
   133                             or if breaking would add only breakgain to space *)
   134            format (es,blockin,after)
   135                (if not force andalso
   136                    pos+wd <= Int.max(#margin (! margin_info) - breakdist(es,after),
   137                                      blockin + #breakgain (! margin_info))
   138                 then blanks wd text  (*just insert wd blanks*)
   139                 else blanks blockin (newline text)));
   140 
   141 
   142 (*** Exported functions to create formatting expressions ***)
   143 
   144 fun length (Block (_, _, len)) = len
   145   | length (String (_, len)) = len
   146   | length (Break(_, wd)) = wd;
   147 
   148 fun str s = String (s, size s);
   149 fun strlen s len = String (s, len);
   150 fun strlen_real s len = strlen s (Real.round len);
   151 val sym = String o apsnd Real.round o Symbol.output_width;
   152 
   153 fun spc n = str (repstring " " n);
   154 
   155 fun brk wd = Break (false, wd);
   156 val fbrk = Break (true, 0);
   157 
   158 fun blk (indent, es) =
   159   let
   160     fun sum([], k) = k
   161       | sum(e :: es, k) = sum (es, length e + k);
   162   in Block (es, indent, sum (es, 0)) end;
   163 
   164 (*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
   165 fun lst(lp,rp) es =
   166   let fun add(e,es) = str"," :: brk 1 :: e :: es;
   167       fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
   168         | list(e::[]) = [str lp, e, str rp]
   169         | list([]) = []
   170   in blk(size lp, list es) end;
   171 
   172 
   173 (* utils *)
   174 
   175 fun quote prt =
   176   blk (1, [str "\"", prt, str "\""]);
   177 
   178 fun commas prts =
   179   flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
   180 
   181 fun breaks prts = separate (brk 1) prts;
   182 
   183 fun fbreaks prts = separate fbrk prts;
   184 
   185 fun block prts = blk (2, prts);
   186 
   187 val strs = block o breaks o (map str);
   188 
   189 fun enclose lpar rpar prts =
   190   block (str lpar :: (prts @ [str rpar]));
   191 
   192 fun list lpar rpar prts =
   193   enclose lpar rpar (commas prts);
   194 
   195 fun str_list lpar rpar strs =
   196   list lpar rpar (map str strs);
   197 
   198 fun big_list name prts =
   199   block (fbreaks (str name :: prts));
   200 
   201 
   202 
   203 (*** Pretty printing with depth limitation ***)
   204 
   205 val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   206 
   207 fun setdepth dp = (depth := dp);
   208 
   209 (*Recursively prune blocks, discarding all text exceeding depth dp*)
   210 fun pruning dp (Block(bes,indent,wd)) =
   211       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   212               else str "..."
   213   | pruning dp e = e;
   214 
   215 fun prune dp e = if dp>0 then pruning dp e else e;
   216 
   217 
   218 fun string_of e = #tx (format ([prune (! depth) e], 0, 0) emptytext);
   219 
   220 val writeln = writeln o string_of;
   221 
   222 
   223 (*Create a single flat string: no line breaking*)
   224 fun str_of prt =
   225   let
   226     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   227       | s_of (String (s, _)) = s
   228       | s_of (Break (false, wd)) = repstring " " wd
   229       | s_of (Break (true, _)) = " ";
   230   in s_of (prune (! depth) prt) end;
   231 
   232 (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
   233 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   234   let
   235     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   236       | pp (String (s, _)) = put_str s
   237       | pp (Break (false, wd)) = put_brk wd
   238       | pp (Break (true, _)) = put_fbrk ()
   239     and pp_lst [] = ()
   240       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   241   in
   242     pp (prune (! depth) prt)
   243   end;
   244 
   245 
   246 end;