src/Pure/Syntax/pretty.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 18 c9ec452ff08f
permissions -rw-r--r--
Initial revision
     1 (*  Title:      Pure/Syntax/pretty
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1991  University of Cambridge
     5 
     6 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 (* FIXME improve? *)
    24 type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) * (unit -> unit);
    25 
    26 signature PRETTY =
    27   sig
    28   type T
    29   val blk : int * T list -> T
    30   val brk : int -> T
    31   val fbrk : T
    32   val str : string -> T
    33   val lst : string * string -> T list -> T
    34   val quote : T -> T
    35   val string_of : T -> string
    36   val str_of : T -> string
    37   val pprint : T -> pprint_args -> unit
    38   val setdepth: int -> unit
    39   val setmargin: int -> unit
    40   end;
    41 
    42 functor PrettyFun () : PRETTY =
    43 struct
    44 
    45 (*Printing items: compound phrases, strings, and breaks*)
    46 datatype T = Block of T list * int * int (*indentation, length*)
    47            | String of string
    48            | Break of bool*int   (*mandatory flag; width if not taken*);
    49 
    50 (*Add the lengths of the expressions until the next Break; if no Break then
    51   include "after", to account for text following this block. *)
    52 fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
    53   | breakdist (String s :: es, after) = size s + breakdist (es, after)
    54   | breakdist (Break _ :: es, after) = 0
    55   | breakdist ([], after) = after;
    56 
    57 fun repstring a 0 = ""
    58   | repstring a 1 = a
    59   | repstring a k =
    60       if k mod 2 = 0 then repstring(a^a) (k div 2)
    61                      else repstring(a^a) (k div 2) ^ a;
    62 
    63 (*** Type for lines of text: string, # of lines, position on line ***)
    64 
    65 type text = {tx: string, nl: int, pos: int};
    66 
    67 val emptytext = {tx="", nl=0, pos=0};
    68 
    69 fun blanks wd {tx,nl,pos} =
    70     {tx  = tx ^ repstring" "wd,
    71      nl  = nl,
    72      pos = pos+wd};
    73 
    74 fun newline {tx,nl,pos} =
    75     {tx  = tx ^ "\n",
    76      nl  = nl+1,
    77      pos = 0};
    78 
    79 fun string s {tx,nl,pos} =
    80     {tx  = tx ^ s,
    81      nl  = nl,
    82      pos = pos + size(s)};
    83 
    84 (*** Formatting ***)
    85 
    86 val margin      = ref 80        (*right margin, or page width*)
    87 and breakgain   = ref 4         (*minimum added space required of a break*)
    88 and emergencypos = ref 40;      (*position too far to right*)
    89 
    90 fun setmargin m =
    91     (margin     := m;
    92      breakgain  := !margin div 20;
    93      emergencypos := !margin div 2);
    94 
    95 fun forcenext [] = []
    96   | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
    97   | forcenext (e :: es) = e :: forcenext es;
    98 
    99 fun format ([], _, _) text = text
   100   | format (e::es, blockin, after) (text as {pos,nl,...}) =
   101     (case e of
   102        Block(bes,indent,wd) =>
   103          let val blockin' = (pos + indent) mod !emergencypos
   104              val btext = format(bes, blockin', breakdist(es,after)) text
   105              val es2 = if nl < #nl(btext) then forcenext es
   106                        else es
   107          in  format (es2,blockin,after) btext  end
   108      | String s => format (es,blockin,after) (string s text)
   109      | Break(force,wd) => (* no break if text fits on this line
   110                       or if breaking would add only breakgain to space *)
   111            format (es,blockin,after)
   112                (if not force andalso
   113                    pos+wd <= max[!margin - breakdist(es,after),
   114                                  blockin + !breakgain]
   115                 then blanks wd text
   116                 else blanks blockin (newline text)));
   117 
   118 (*** Exported functions to create formatting expressions ***)
   119 
   120 fun length (Block(_,_,len)) = len
   121   | length (String s) = size s
   122   | length (Break(_,wd)) = wd;
   123 
   124 val str = String
   125 and fbrk = Break(true,0);
   126 
   127 fun brk wd = Break(false,wd);
   128 
   129 fun blk (indent,es) =
   130   let fun sum([], k) = k
   131         | sum(e::es, k) = sum(es, length e + k)
   132   in  Block(es,indent, sum(es,0))  end;
   133 
   134 fun lst(lp,rp) es =
   135   let fun add(e,es) = str"," :: brk 1 :: e :: es;
   136       fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
   137         | list(e::[]) = [str lp, e, str rp]
   138         | list([]) = []
   139   in blk(size lp, list es) end;
   140 
   141 fun quote prt = blk (1, [str "\"", prt, str "\""]);
   142 
   143 
   144 (*** Pretty printing with depth limitation ***)
   145 
   146 val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   147 
   148 fun setdepth dp = (depth := dp);
   149 
   150 
   151 fun pruning dp (Block(bes,indent,wd)) =
   152       if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   153               else String"..."
   154   | pruning dp e = e;
   155 
   156 fun prune dp e = if dp>0 then pruning dp e else e;
   157 
   158 
   159 fun string_of e = #tx (format ([prune (!depth) e],0,0) emptytext);
   160 
   161 
   162 fun brk_width (force, wd) = if force andalso wd = 0 then 1 else wd;
   163 
   164 fun str_of prt =
   165   let
   166     fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   167       | s_of (String s) = s
   168       | s_of (Break f_w) = repstring " " (brk_width f_w);
   169   in
   170     s_of (prune (! depth) prt)
   171   end;
   172 
   173 
   174 fun pprint prt (put_str, begin_blk, put_brk, end_blk) =
   175   let
   176     fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   177       | pp (String s) = put_str s
   178       | pp (Break f_w) = put_brk (brk_width f_w)
   179     and pp_lst [] = ()
   180       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   181   in
   182     pp (prune (! depth) prt)
   183   end;
   184 
   185 
   186 (*** Initialization ***)
   187 
   188 val () = setmargin 80;
   189 
   190 end;
   191