src/Pure/General/pretty.ML
author wenzelm
Thu Feb 11 21:15:46 1999 +0100 (1999-02-11)
changeset 6271 957d8aa4a06b
parent 6118 caa439435666
child 6321 207f518167e8
permissions -rw-r--r--
sym: Symbol.output_width;
     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 str: string -> T
    30   val strlen: string -> int -> T
    31   val sym: string -> T
    32   val spc: int -> T
    33   val brk: int -> T
    34   val fbrk: T
    35   val blk: int * T list -> T
    36   val lst: string * string -> T list -> T
    37   val quote: T -> T
    38   val commas: T list -> T list
    39   val breaks: T list -> T list
    40   val fbreaks: T list -> T list
    41   val block: T list -> T
    42   val strs: string list -> T
    43   val enclose: string -> string -> T list -> T
    44   val list: string -> string -> T list -> T
    45   val str_list: string -> string -> string list -> T
    46   val big_list: string -> T list -> 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   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: string, nl: int, pos: int};
    80 
    81 val emptytext = {tx="", nl=0, pos=0};
    82 
    83 fun blanks wd {tx,nl,pos} =
    84     {tx  = tx ^ repstring " " wd,
    85      nl  = nl,
    86      pos = pos+wd};
    87 
    88 fun newline {tx,nl,pos} =
    89     {tx  = tx ^ "\n",
    90      nl  = nl+1,
    91      pos = 0};
    92 
    93 fun string s len {tx,nl,pos:int} =
    94     {tx  = tx ^ s,
    95      nl  = nl,
    96      pos = pos + len};
    97 
    98 
    99 (*** Formatting ***)
   100 
   101 (* margin *)
   102 
   103 (*example values*)
   104 val margin      = ref 80        (*right margin, or page width*)
   105 and breakgain   = ref 4         (*minimum added space required of a break*)
   106 and emergencypos = ref 40;      (*position too far to right*)
   107 
   108 fun setmargin m =
   109     (margin     := m;
   110      breakgain  := !margin div 20;
   111      emergencypos := !margin div 2);
   112 
   113 val () = setmargin 76;
   114 
   115 
   116 (*Search for the next break (at this or higher levels) and force it to occur*)
   117 fun forcenext [] = []
   118   | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   119   | forcenext (e :: es) = e :: forcenext es;
   120 
   121 (*es is list of expressions to print;
   122   blockin is the indentation of the current block;
   123   after is the width of the following context until next break. *)
   124 fun format ([], _, _) text = text
   125   | format (e::es, blockin, after) (text as {pos,nl,...}) =
   126     (case e of
   127        Block(bes,indent,wd) =>
   128          let val blockin' = (pos + indent) mod !emergencypos
   129              val btext = format(bes, blockin', breakdist(es,after)) text
   130              (*If this block was broken then force the next break.*)
   131              val es2 = if nl < #nl(btext) then forcenext es else es
   132          in  format (es2,blockin,after) btext  end
   133      | String (s, len) => format (es,blockin,after) (string s len text)
   134      | Break(force,wd) => (*no break if text to next break fits on this line
   135                             or if breaking would add only breakgain to space *)
   136            format (es,blockin,after)
   137                (if not force andalso
   138                    pos+wd <= Int.max(!margin - breakdist(es,after),
   139                                      blockin + !breakgain)
   140                 then blanks wd text  (*just insert wd blanks*)
   141                 else blanks blockin (newline text)));
   142 
   143 
   144 (*** Exported functions to create formatting expressions ***)
   145 
   146 fun length (Block (_, _, len)) = len
   147   | length (String (_, len)) = len
   148   | length (Break(_, wd)) = wd;
   149 
   150 fun str s = String (s, size s);
   151 fun strlen s len = String (s, len);
   152 val sym = String o apsnd Real.round o Symbol.output_width;
   153 
   154 fun spc n = str (repstring " " n);
   155 
   156 fun brk wd = Break (false, wd);
   157 val fbrk = Break (true, 0);
   158 
   159 fun blk (indent, es) =
   160   let
   161     fun sum([], k) = k
   162       | sum(e :: es, k) = sum (es, length e + k);
   163   in Block (es, indent, sum (es, 0)) end;
   164 
   165 (*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
   166 fun lst(lp,rp) es =
   167   let fun add(e,es) = str"," :: brk 1 :: e :: es;
   168       fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
   169         | list(e::[]) = [str lp, e, str rp]
   170         | list([]) = []
   171   in blk(size lp, list es) end;
   172 
   173 
   174 (* utils *)
   175 
   176 fun quote prt =
   177   blk (1, [str "\"", prt, str "\""]);
   178 
   179 fun commas prts =
   180   flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
   181 
   182 fun breaks prts = separate (brk 1) prts;
   183 
   184 fun fbreaks prts = separate fbrk prts;
   185 
   186 fun block prts = blk (2, prts);
   187 
   188 val strs = block o breaks o (map str);
   189 
   190 fun enclose lpar rpar prts =
   191   block (str lpar :: (prts @ [str rpar]));
   192 
   193 fun list lpar rpar prts =
   194   enclose lpar rpar (commas prts);
   195 
   196 fun str_list lpar rpar strs =
   197   list lpar rpar (map str strs);
   198 
   199 fun big_list name prts =
   200   block (fbreaks (str name :: prts));
   201 
   202 
   203 
   204 (*** Pretty printing with depth limitation ***)
   205 
   206 val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   207 
   208 fun setdepth dp = (depth := dp);
   209 
   210 (*Recursively prune blocks, discarding all text exceeding depth dp*)
   211 fun pruning dp (Block(bes,indent,wd)) =
   212       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   213               else str "..."
   214   | pruning dp e = e;
   215 
   216 fun prune dp e = if dp>0 then pruning dp e else e;
   217 
   218 
   219 fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
   220 
   221 val writeln = writeln o string_of;
   222 
   223 
   224 (*Create a single flat string: no line breaking*)
   225 fun str_of prt =
   226   let
   227     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   228       | s_of (String (s, _)) = s
   229       | s_of (Break (false, wd)) = repstring " " wd
   230       | s_of (Break (true, _)) = " ";
   231   in
   232     s_of (prune (! depth) prt)
   233   end;
   234 
   235 (*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
   236 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   237   let
   238     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   239       | pp (String (s, _)) = put_str s
   240       | pp (Break (false, wd)) = put_brk wd
   241       | pp (Break (true, _)) = put_fbrk ()
   242     and pp_lst [] = ()
   243       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   244   in
   245     pp (prune (! depth) prt)
   246   end;
   247 
   248 
   249 end;