src/Pure/General/pretty.ML
author wenzelm
Wed Mar 15 18:18:12 2000 +0100 (2000-03-15)
changeset 8456 8ccda76f07cb
parent 6321 207f518167e8
child 8806 a202293db3f6
permissions -rw-r--r--
removed lst, strlen, strlen_real, spc, sym;
added chunks, raw_str;
pass all strings through Symbol.output (beware: this is done at
different times for str and spacing/linebreaks!);
speedup formatting (uses Buffer.T);
tuned;
     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 raw_str: string * real -> T
    30   val str: string -> T
    31   val brk: int -> T
    32   val fbrk: T
    33   val blk: int * T list -> T
    34   val quote: T -> T
    35   val commas: T list -> T list
    36   val breaks: T list -> T list
    37   val fbreaks: T list -> T list
    38   val block: T list -> T
    39   val strs: string list -> T
    40   val enclose: string -> string -> T list -> T
    41   val list: string -> string -> T list -> T
    42   val str_list: string -> string -> string list -> T
    43   val big_list: string -> T list -> T
    44   val chunks: T list -> T
    45   val string_of: T -> string
    46   val writeln: T -> unit
    47   val str_of: T -> string
    48   val pprint: T -> pprint_args -> unit
    49   val setdepth: int -> unit
    50   val setmargin: int -> unit
    51   val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    52   end;
    53 
    54 structure Pretty : PRETTY =
    55 struct
    56 
    57 (*printing items: compound phrases, strings, and breaks*)
    58 datatype T =
    59   Block of T list * int * int |         (*body, indentation, length*)
    60   String of string * int |              (*text, length*)
    61   Break of bool * int;                  (*mandatory flag, width if not taken*);
    62 
    63 (*Add the lengths of the expressions until the next Break; if no Break then
    64   include "after", to account for text following this block. *)
    65 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
    66   | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
    67   | breakdist (Break _ :: es, after) = 0
    68   | breakdist ([], after) = after;
    69 
    70 fun repstring a 0 = ""
    71   | repstring a 1 = a
    72   | repstring a k =
    73       if k mod 2 = 0 then repstring(a^a) (k div 2)
    74                      else repstring(a^a) (k div 2) ^ a;
    75 
    76 (*** Type for lines of text: string, # of lines, position on line ***)
    77 
    78 type text = {tx: Buffer.T, nl: int, pos: int};
    79 
    80 val emptytext = {tx = Buffer.empty, nl = 0, pos = 0};
    81 
    82 fun blanks wd {tx, nl, pos} =
    83     {tx  = Buffer.add (Symbol.output (repstring " " wd)) tx,
    84      nl  = nl,
    85      pos = pos+wd};
    86 
    87 fun newline {tx, nl, pos} =
    88     {tx  = Buffer.add (Symbol.output "\n") tx,
    89      nl  = nl + 1,
    90      pos = 0};
    91 
    92 fun string s len {tx, nl, pos:int} =
    93     {tx  = Buffer.add s tx,
    94      nl  = nl,
    95      pos = pos + len};
    96 
    97 
    98 (*** Formatting ***)
    99 
   100 (* margin *)
   101 
   102 fun make_margin_info m =
   103  {margin = m,                   (*right margin, or page width*)
   104   breakgain = m div 20,         (*minimum added space required of a break*)
   105   emergencypos = m div 2};      (*position too far to right*)
   106 
   107 val margin_info = ref (make_margin_info 76);
   108 fun setmargin m = margin_info := make_margin_info m;
   109 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
   110 
   111 (*Search for the next break (at this or higher levels) and force it to occur*)
   112 fun forcenext [] = []
   113   | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   114   | forcenext (e :: es) = e :: forcenext es;
   115 
   116 (*es is list of expressions to print;
   117   blockin is the indentation of the current block;
   118   after is the width of the following context until next break. *)
   119 fun format ([], _, _) text = text
   120   | format (e::es, blockin, after) (text as {pos,nl,...}) =
   121     (case e of
   122        Block(bes,indent,wd) =>
   123          let val blockin' = (pos + indent) mod #emergencypos (! margin_info)
   124              val btext = format(bes, blockin', breakdist(es,after)) text
   125              (*If this block was broken then force the next break.*)
   126              val es2 = if nl < #nl(btext) then forcenext es else es
   127          in  format (es2,blockin,after) btext  end
   128      | String (s, len) => format (es,blockin,after) (string s len text)
   129      | Break(force,wd) => (*no break if text to next break fits on this line
   130                             or if breaking would add only breakgain to space *)
   131            format (es,blockin,after)
   132                (if not force andalso
   133                    pos+wd <= Int.max(#margin (! margin_info) - breakdist(es,after),
   134                                      blockin + #breakgain (! margin_info))
   135                 then blanks wd text  (*just insert wd blanks*)
   136                 else blanks blockin (newline text)));
   137 
   138 
   139 (*** Exported functions to create formatting expressions ***)
   140 
   141 fun length (Block (_, _, len)) = len
   142   | length (String (_, len)) = len
   143   | length (Break(_, wd)) = wd;
   144 
   145 fun raw_str (s, len) = String (s, Real.round len);
   146 val str = String o apsnd Real.round o Symbol.output_width;
   147 
   148 fun brk wd = Break (false, wd);
   149 val fbrk = Break (true, 0);
   150 
   151 fun blk (indent, es) =
   152   let
   153     fun sum([], k) = k
   154       | sum(e :: es, k) = sum (es, length e + k);
   155   in Block (es, indent, sum (es, 0)) end;
   156 
   157 
   158 (* utils *)
   159 
   160 fun quote prt =
   161   blk (1, [str "\"", prt, str "\""]);
   162 
   163 fun commas prts =
   164   flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
   165 
   166 fun breaks prts = separate (brk 1) prts;
   167 fun fbreaks prts = separate fbrk prts;
   168 
   169 fun block prts = blk (2, prts);
   170 
   171 val strs = block o breaks o (map str);
   172 
   173 fun enclose lpar rpar prts =
   174   block (str lpar :: (prts @ [str rpar]));
   175 
   176 fun list lpar rpar prts = enclose lpar rpar (commas prts);
   177 fun str_list lpar rpar strs = list lpar rpar (map str strs);
   178 fun big_list name prts = block (fbreaks (str name :: prts));
   179 fun chunks prts = blk (0, fbreaks prts);
   180 
   181 
   182 (*** Pretty printing with depth limitation ***)
   183 
   184 val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   185 
   186 fun setdepth dp = (depth := dp);
   187 
   188 (*Recursively prune blocks, discarding all text exceeding depth dp*)
   189 fun pruning dp (Block(bes,indent,wd)) =
   190       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   191               else str "..."
   192   | pruning dp e = e;
   193 
   194 fun prune dp e = if dp>0 then pruning dp e else e;
   195 
   196 
   197 fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], 0, 0) emptytext));
   198 
   199 val writeln = writeln o string_of;
   200 
   201 
   202 (*Create a single flat string: no line breaking*)
   203 fun str_of prt =
   204   let
   205     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   206       | s_of (String (s, _)) = s
   207       | s_of (Break (false, wd)) = Symbol.output (repstring " " wd)
   208       | s_of (Break (true, _)) = Symbol.output " ";
   209   in s_of (prune (! depth) prt) end;
   210 
   211 (*part of the interface to the ML toplevel pretty printers*)
   212 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   213   let
   214     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   215       | pp (String (s, _)) = put_str s
   216       | pp (Break (false, wd)) = put_brk wd
   217       | pp (Break (true, _)) = put_fbrk ()
   218     and pp_lst [] = ()
   219       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   220   in
   221     pp (prune (! depth) prt)
   222   end;
   223 
   224 
   225 end;