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