src/Pure/General/pretty.ML
author wenzelm
Sat Dec 08 14:42:45 2001 +0100 (2001-12-08)
changeset 12421 54c06c1f88b8
parent 10952 b520e4f1313b
child 14832 6589a58f57cb
permissions -rw-r--r--
added writelns;
     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 indent: int -> T -> T
    47   val string_of: T -> string
    48   val writeln: T -> unit
    49   val writelns: T list -> 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 
    61 (** printing items: compound phrases, strings, and breaks **)
    62 
    63 datatype T =
    64   Block of T list * int * int |         (*body, indentation, length*)
    65   String of string * int |              (*text, length*)
    66   Break of bool * int;                  (*mandatory flag, width if not taken*);
    67 
    68 
    69 
    70 (** output text **)
    71 
    72 val output_spaces = Symbol.output o Symbol.spaces;
    73 val add_indent = Buffer.add o output_spaces;
    74 fun set_indent wd = Buffer.empty |> add_indent wd;
    75 
    76 val empty =
    77  {tx = Buffer.empty,
    78   ind = Buffer.empty,
    79   pos = 0,
    80   nl = 0};
    81 
    82 fun newline {tx, ind, pos, nl} =
    83  {tx = Buffer.add (Symbol.output "\n") tx,
    84   ind = Buffer.empty,
    85   pos = 0,
    86   nl = nl + 1};
    87 
    88 fun string (s, len) {tx, ind, pos: int, nl} =
    89  {tx = Buffer.add s tx,
    90   ind = Buffer.add s ind,
    91   pos = pos + len,
    92   nl = nl};
    93 
    94 fun blanks wd = string (output_spaces wd, wd);
    95 
    96 fun indentation (buf, len) {tx, ind, pos, nl} =
    97   let val s = Buffer.content buf in
    98    {tx = Buffer.add (Symbol.indent (s, len)) tx,
    99     ind = Buffer.add s ind,
   100     pos = pos + len,
   101     nl = nl}
   102   end;
   103 
   104 
   105 
   106 (** formatting **)
   107 
   108 (* margin *)
   109 
   110 fun make_margin_info m =
   111  {margin = m,                   (*right margin, or page width*)
   112   breakgain = m div 20,         (*minimum added space required of a break*)
   113   emergencypos = m div 2};      (*position too far to right*)
   114 
   115 val margin_info = ref (make_margin_info 76);
   116 fun setmargin m = margin_info := make_margin_info m;
   117 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
   118 
   119 
   120 (* format *)
   121 
   122 (*Add the lengths of the expressions until the next Break; if no Break then
   123   include "after", to account for text following this block.*)
   124 fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after)
   125   | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
   126   | breakdist (Break _ :: es, after) = 0
   127   | breakdist ([], after) = after;
   128 
   129 (*Search for the next break (at this or higher levels) and force it to occur.*)
   130 fun forcenext [] = []
   131   | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
   132   | forcenext (e :: es) = e :: forcenext es;
   133 
   134 (*es is list of expressions to print;
   135   blockin is the indentation of the current block;
   136   after is the width of the following context until next break.*)
   137 fun format ([], _, _) text = text
   138   | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
   139       (case e of
   140         Block (bes, indent, wd) =>
   141           let
   142             val {emergencypos, ...} = ! margin_info;
   143             val pos' = pos + indent;
   144             val pos'' = pos' mod emergencypos;
   145             val block' =
   146               if pos' < emergencypos then (ind |> add_indent indent, pos')
   147               else (set_indent pos'', pos'');
   148             val btext = format (bes, block', breakdist (es, after)) text;
   149             (*if this block was broken then force the next break*)
   150             val es2 = if nl < #nl btext then forcenext es else es;
   151           in format (es2, block, after) btext end
   152       | String str => format (es, block, after) (string str text)
   153       | Break (force, wd) =>
   154           let val {margin, breakgain, ...} = ! margin_info in
   155             (*no break if text to next break fits on this line
   156               or if breaking would add only breakgain to space*)
   157             format (es, block, after)
   158               (if not force andalso
   159                   pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   160                 then text |> blanks wd  (*just insert wd blanks*)
   161                 else text |> newline |> indentation block)
   162           end);
   163 
   164 
   165 (*** Exported functions to create formatting expressions ***)
   166 
   167 fun length (Block (_, _, len)) = len
   168   | length (String (_, len)) = len
   169   | length (Break(_, wd)) = wd;
   170 
   171 fun raw_str (s, len) = String (s, Real.round len);
   172 val str = String o apsnd Real.round o Symbol.output_width;
   173 
   174 fun brk wd = Break (false, wd);
   175 val fbrk = Break (true, 2);
   176 
   177 fun blk (indent, es) =
   178   let
   179     fun sum([], k) = k
   180       | sum(e :: es, k) = sum (es, length e + k);
   181   in Block (es, indent, sum (es, 0)) end;
   182 
   183 
   184 (* utils *)
   185 
   186 fun quote prt =
   187   blk (1, [str "\"", prt, str "\""]);
   188 
   189 fun commas prts =
   190   flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
   191 
   192 fun breaks prts = separate (brk 1) prts;
   193 fun fbreaks prts = separate fbrk prts;
   194 
   195 fun block prts = blk (2, prts);
   196 
   197 val strs = block o breaks o map str;
   198 
   199 fun enclose lpar rpar prts =
   200   block (str lpar :: (prts @ [str rpar]));
   201 
   202 fun list lpar rpar prts = enclose lpar rpar (commas prts);
   203 fun str_list lpar rpar strs = list lpar rpar (map str strs);
   204 fun big_list name prts = block (fbreaks (str name :: prts));
   205 fun chunks prts = blk (0, fbreaks prts);
   206 
   207 fun indent 0 prt = prt
   208   | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
   209 
   210 
   211 (*** Pretty printing with depth limitation ***)
   212 
   213 val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   214 
   215 fun setdepth dp = (depth := dp);
   216 
   217 (*Recursively prune blocks, discarding all text exceeding depth dp*)
   218 fun pruning dp (Block(bes,indent,wd)) =
   219       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   220               else str "..."
   221   | pruning dp e = e;
   222 
   223 fun prune dp e = if dp > 0 then pruning dp e else e;
   224 
   225 fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
   226 val writeln = writeln o string_of;
   227 fun writelns [] = () | writelns es = writeln (chunks es);
   228 
   229 
   230 (*Create a single flat string: no line breaking*)
   231 fun str_of prt =
   232   let
   233     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   234       | s_of (String (s, _)) = s
   235       | s_of (Break (false, wd)) = output_spaces wd
   236       | s_of (Break (true, _)) = output_spaces 1;
   237   in s_of (prune (! depth) prt) end;
   238 
   239 (*part of the interface to the ML toplevel pretty printers*)
   240 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   241   let
   242     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   243       | pp (String (s, _)) = put_str s
   244       | pp (Break (false, wd)) = put_brk wd
   245       | pp (Break (true, _)) = put_fbrk ()
   246     and pp_lst [] = ()
   247       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   248   in
   249     pp (prune (! depth) prt)
   250   end;
   251 
   252 
   253 end;