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