src/Pure/General/pretty.ML
author haftmann
Wed Sep 21 10:39:38 2005 +0200 (2005-09-21)
changeset 17542 b588e06b6775
parent 17526 8d7c587c6b34
child 17756 d4a35f82fbb4
permissions -rw-r--r--
(name mess cleanup)
     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 
     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 unbreakable: T -> 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 gen_list: string -> string -> string -> T list -> T
    44   val str_list: string -> string -> string list -> T
    45   val big_list: string -> T list -> T
    46   val chunks: T list -> T
    47   val indent: int -> T -> T
    48   val string_of: T -> string
    49   val output_buffer: T -> Buffer.T
    50   val output: T -> string
    51   val writeln: T -> unit
    52   val writelns: T list -> unit
    53   val str_of: T -> string
    54   val pprint: T -> pprint_args -> unit
    55   val setdepth: int -> unit
    56   val setmargin: int -> unit
    57   val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    58   type pp
    59   val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
    60   val term: pp -> term -> T
    61   val typ: pp -> typ -> T
    62   val sort: pp -> sort -> T
    63   val classrel: pp -> class list -> T
    64   val arity: pp -> arity -> T
    65   val string_of_term: pp -> term -> string
    66   val string_of_typ: pp -> typ -> string
    67   val string_of_sort: pp -> sort -> string
    68   val string_of_classrel: pp -> class list -> string
    69   val string_of_arity: pp -> arity -> string
    70 end;
    71 
    72 structure Pretty : PRETTY =
    73 struct
    74 
    75 
    76 (** printing items: compound phrases, strings, and breaks **)
    77 
    78 datatype T =
    79   Block of T list * int * int |         (*body, indentation, length*)
    80   String of string * int |              (*text, length*)
    81   Break of bool * int;                  (*mandatory flag, width if not taken*);
    82 
    83 
    84 
    85 (** output text **)
    86 
    87 val output_spaces = Output.output o Symbol.spaces;
    88 val add_indent = Buffer.add o output_spaces;
    89 fun set_indent wd = Buffer.empty |> add_indent wd;
    90 
    91 val empty =
    92  {tx = Buffer.empty,
    93   ind = Buffer.empty,
    94   pos = 0,
    95   nl = 0};
    96 
    97 fun newline {tx, ind, pos, nl} =
    98  {tx = Buffer.add (Output.output "\n") tx,
    99   ind = Buffer.empty,
   100   pos = 0,
   101   nl = nl + 1};
   102 
   103 fun string (s, len) {tx, ind, pos: int, nl} =
   104  {tx = Buffer.add s tx,
   105   ind = Buffer.add s ind,
   106   pos = pos + len,
   107   nl = nl};
   108 
   109 fun blanks wd = string (output_spaces wd, wd);
   110 
   111 fun indentation (buf, len) {tx, ind, pos, nl} =
   112   let val s = Buffer.content buf in
   113    {tx = Buffer.add (Output.indent (s, len)) tx,
   114     ind = Buffer.add s ind,
   115     pos = pos + len,
   116     nl = nl}
   117   end;
   118 
   119 
   120 
   121 (** formatting **)
   122 
   123 (* margin *)
   124 
   125 fun make_margin_info m =
   126  {margin = m,                   (*right margin, or page width*)
   127   breakgain = m div 20,         (*minimum added space required of a break*)
   128   emergencypos = m div 2};      (*position too far to right*)
   129 
   130 val margin_info = ref (make_margin_info 76);
   131 fun setmargin m = margin_info := make_margin_info m;
   132 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
   133 
   134 
   135 (* format *)
   136 
   137 (*Add the lengths of the expressions until the next Break; if no Break then
   138   include "after", to account for text following this block.*)
   139 fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after)
   140   | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
   141   | breakdist (Break _ :: es, after) = 0
   142   | breakdist ([], after) = after;
   143 
   144 (*Search for the next break (at this or higher levels) and force it to occur.*)
   145 fun forcenext [] = []
   146   | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
   147   | forcenext (e :: es) = e :: forcenext es;
   148 
   149 (*es is list of expressions to print;
   150   blockin is the indentation of the current block;
   151   after is the width of the following context until next break.*)
   152 fun format ([], _, _) text = text
   153   | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
   154       (case e of
   155         Block (bes, indent, wd) =>
   156           let
   157             val {emergencypos, ...} = ! margin_info;
   158             val pos' = pos + indent;
   159             val pos'' = pos' mod emergencypos;
   160             val block' =
   161               if pos' < emergencypos then (ind |> add_indent indent, pos')
   162               else (set_indent pos'', pos'');
   163             val btext = format (bes, block', breakdist (es, after)) text;
   164             (*if this block was broken then force the next break*)
   165             val es2 = if nl < #nl btext then forcenext es else es;
   166           in format (es2, block, after) btext end
   167       | String str => format (es, block, after) (string str text)
   168       | Break (force, wd) =>
   169           let val {margin, breakgain, ...} = ! margin_info in
   170             (*no break if text to next break fits on this line
   171               or if breaking would add only breakgain to space*)
   172             format (es, block, after)
   173               (if not force andalso
   174                   pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   175                 then text |> blanks wd  (*just insert wd blanks*)
   176                 else text |> newline |> indentation block)
   177           end);
   178 
   179 
   180 (** Exported functions to create formatting expressions **)
   181 
   182 fun length (Block (_, _, len)) = len
   183   | length (String (_, len)) = len
   184   | length (Break(_, wd)) = wd;
   185 
   186 fun raw_str (s, len) = String (s, Real.round len);
   187 val str = String o apsnd Real.round o Output.output_width;
   188 
   189 fun brk wd = Break (false, wd);
   190 val fbrk = Break (true, 2);
   191 
   192 fun blk (indent, es) =
   193   let
   194     fun sum([], k) = k
   195       | sum(e :: es, k) = sum (es, length e + k);
   196   in Block (es, indent, sum (es, 0)) end;
   197 
   198 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
   199   | unbreakable (Block (es, indent, wd)) = Block (map unbreakable es, indent, wd)
   200   | unbreakable (e as String _) = e;
   201 
   202 
   203 (* utils *)
   204 
   205 fun quote prt =
   206   blk (1, [str "\"", prt, str "\""]);
   207 
   208 fun separate_pretty sep prts =
   209   prts
   210   |> map single
   211   |> separate [str sep, brk 1]
   212   |> List.concat;
   213 
   214 val commas = separate_pretty ",";
   215 
   216 fun breaks prts = separate (brk 1) prts;
   217 fun fbreaks prts = separate fbrk prts;
   218 
   219 fun block prts = blk (2, prts);
   220 
   221 val strs = block o breaks o map str;
   222 
   223 fun enclose lpar rpar prts =
   224   block (str lpar :: (prts @ [str rpar]));
   225 
   226 fun gen_list sep lpar rpar prts = enclose lpar rpar (separate_pretty sep prts);
   227 val list = gen_list ",";
   228 fun str_list lpar rpar strs = list lpar rpar (map str strs);
   229 fun big_list name prts = block (fbreaks (str name :: prts));
   230 fun chunks prts = blk (0, fbreaks prts);
   231 
   232 fun indent 0 prt = prt
   233   | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
   234 
   235 
   236 
   237 (** Pretty printing with depth limitation **)
   238 
   239 val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   240 
   241 fun setdepth dp = (depth := dp);
   242 
   243 (*Recursively prune blocks, discarding all text exceeding depth dp*)
   244 fun pruning dp (Block(bes,indent,wd)) =
   245       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   246               else str "..."
   247   | pruning dp e = e;
   248 
   249 fun prune dp e = if dp > 0 then pruning dp e else e;
   250 
   251 fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);
   252 val output = Buffer.content o output_buffer;
   253 val string_of = Output.raw o output;
   254 val writeln = Output.writeln o string_of;
   255 fun writelns [] = () | writelns es = writeln (chunks es);
   256 
   257 
   258 (*Create a single flat string: no line breaking*)
   259 fun str_of prt =
   260   let
   261     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   262       | s_of (String (s, _)) = s
   263       | s_of (Break (false, wd)) = output_spaces wd
   264       | s_of (Break (true, _)) = output_spaces 1;
   265   in Output.raw (s_of (prune (! depth) prt)) end;
   266 
   267 (*part of the interface to the ML toplevel pretty printers*)
   268 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   269   let
   270     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   271       | pp (String (s, _)) = put_str s
   272       | pp (Break (false, wd)) = put_brk wd
   273       | pp (Break (true, _)) = put_fbrk ()
   274     and pp_lst [] = ()
   275       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   276   in
   277     pp (prune (! depth) prt)
   278   end;
   279 
   280 
   281 
   282 (** abstract pretty printing context **)
   283 
   284 datatype pp =
   285   PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
   286 
   287 val pp = PP;
   288 
   289 fun pp_fun f (PP x) = f x;
   290 
   291 val term     = pp_fun #1;
   292 val typ      = pp_fun #2;
   293 val sort     = pp_fun #3;
   294 val classrel = pp_fun #4;
   295 val arity    = pp_fun #5;
   296 
   297 val string_of_term     = string_of oo term;
   298 val string_of_typ      = string_of oo typ;
   299 val string_of_sort     = string_of oo sort;
   300 val string_of_classrel = string_of oo classrel;
   301 val string_of_arity    = string_of oo arity;
   302 
   303 end;