src/Pure/General/pretty.ML
author wenzelm
Tue Mar 09 12:11:00 1999 +0100 (1999-03-09)
changeset 6321 207f518167e8
parent 6271 957d8aa4a06b
child 8456 8ccda76f07cb
permissions -rw-r--r--
added strlen_real, setmp_margin;
wenzelm@6118
     1
(*  Title:      Pure/General/pretty.ML
wenzelm@6116
     2
    ID:         $Id$
wenzelm@6116
     3
    Author:     Lawrence C Paulson
wenzelm@6116
     4
    Copyright   1991  University of Cambridge
wenzelm@6116
     5
wenzelm@6116
     6
Generic pretty printing module.
wenzelm@6116
     7
wenzelm@6116
     8
Loosely based on
wenzelm@6116
     9
  D. C. Oppen, "Pretty Printing",
wenzelm@6116
    10
  ACM Transactions on Programming Languages and Systems (1980), 465-483.
wenzelm@6116
    11
wenzelm@6116
    12
The object to be printed is given as a tree with indentation and line
wenzelm@6116
    13
breaking information.  A "break" inserts a newline if the text until
wenzelm@6116
    14
the next break is too long to fit on the current line.  After the newline,
wenzelm@6116
    15
text is indented to the level of the enclosing block.  Normally, if a block
wenzelm@6116
    16
is broken then all enclosing blocks will also be broken.  Only "inconsistent
wenzelm@6116
    17
breaks" are provided.
wenzelm@6116
    18
wenzelm@6116
    19
The stored length of a block is used in breakdist (to treat each inner block as
wenzelm@6116
    20
a unit for breaking).
wenzelm@6116
    21
*)
wenzelm@6116
    22
wenzelm@6116
    23
type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
wenzelm@6116
    24
  (unit -> unit) * (unit -> unit);
wenzelm@6116
    25
wenzelm@6116
    26
signature PRETTY =
wenzelm@6116
    27
  sig
wenzelm@6116
    28
  type T
wenzelm@6116
    29
  val str: string -> T
wenzelm@6116
    30
  val strlen: string -> int -> T
wenzelm@6321
    31
  val strlen_real: string -> real -> T
wenzelm@6116
    32
  val sym: string -> T
wenzelm@6116
    33
  val spc: int -> T
wenzelm@6116
    34
  val brk: int -> T
wenzelm@6116
    35
  val fbrk: T
wenzelm@6116
    36
  val blk: int * T list -> T
wenzelm@6116
    37
  val lst: string * string -> T list -> T
wenzelm@6116
    38
  val quote: T -> T
wenzelm@6116
    39
  val commas: T list -> T list
wenzelm@6116
    40
  val breaks: T list -> T list
wenzelm@6116
    41
  val fbreaks: T list -> T list
wenzelm@6116
    42
  val block: T list -> T
wenzelm@6116
    43
  val strs: string list -> T
wenzelm@6116
    44
  val enclose: string -> string -> T list -> T
wenzelm@6116
    45
  val list: string -> string -> T list -> T
wenzelm@6116
    46
  val str_list: string -> string -> string list -> T
wenzelm@6116
    47
  val big_list: string -> T list -> T
wenzelm@6116
    48
  val string_of: T -> string
wenzelm@6116
    49
  val writeln: T -> unit
wenzelm@6116
    50
  val str_of: T -> string
wenzelm@6116
    51
  val pprint: T -> pprint_args -> unit
wenzelm@6116
    52
  val setdepth: int -> unit
wenzelm@6116
    53
  val setmargin: int -> unit
wenzelm@6321
    54
  val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
wenzelm@6116
    55
  end;
wenzelm@6116
    56
wenzelm@6116
    57
structure Pretty : PRETTY =
wenzelm@6116
    58
struct
wenzelm@6116
    59
wenzelm@6116
    60
(*printing items: compound phrases, strings, and breaks*)
wenzelm@6116
    61
datatype T =
wenzelm@6116
    62
  Block of T list * int * int |         (*body, indentation, length*)
wenzelm@6116
    63
  String of string * int |              (*text, length*)
wenzelm@6116
    64
  Break of bool * int;                  (*mandatory flag, width if not taken*);
wenzelm@6116
    65
wenzelm@6116
    66
(*Add the lengths of the expressions until the next Break; if no Break then
wenzelm@6116
    67
  include "after", to account for text following this block. *)
wenzelm@6116
    68
fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
wenzelm@6116
    69
  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
wenzelm@6116
    70
  | breakdist (Break _ :: es, after) = 0
wenzelm@6116
    71
  | breakdist ([], after) = after;
wenzelm@6116
    72
wenzelm@6116
    73
fun repstring a 0 = ""
wenzelm@6116
    74
  | repstring a 1 = a
wenzelm@6116
    75
  | repstring a k =
wenzelm@6116
    76
      if k mod 2 = 0 then repstring(a^a) (k div 2)
wenzelm@6116
    77
                     else repstring(a^a) (k div 2) ^ a;
wenzelm@6116
    78
wenzelm@6116
    79
(*** Type for lines of text: string, # of lines, position on line ***)
wenzelm@6116
    80
wenzelm@6116
    81
type text = {tx: string, nl: int, pos: int};
wenzelm@6116
    82
wenzelm@6116
    83
val emptytext = {tx="", nl=0, pos=0};
wenzelm@6116
    84
wenzelm@6116
    85
fun blanks wd {tx,nl,pos} =
wenzelm@6116
    86
    {tx  = tx ^ repstring " " wd,
wenzelm@6116
    87
     nl  = nl,
wenzelm@6116
    88
     pos = pos+wd};
wenzelm@6116
    89
wenzelm@6116
    90
fun newline {tx,nl,pos} =
wenzelm@6116
    91
    {tx  = tx ^ "\n",
wenzelm@6116
    92
     nl  = nl+1,
wenzelm@6116
    93
     pos = 0};
wenzelm@6116
    94
wenzelm@6116
    95
fun string s len {tx,nl,pos:int} =
wenzelm@6116
    96
    {tx  = tx ^ s,
wenzelm@6116
    97
     nl  = nl,
wenzelm@6116
    98
     pos = pos + len};
wenzelm@6116
    99
wenzelm@6116
   100
wenzelm@6116
   101
(*** Formatting ***)
wenzelm@6116
   102
wenzelm@6116
   103
(* margin *)
wenzelm@6116
   104
wenzelm@6321
   105
fun make_margin_info m =
wenzelm@6321
   106
 {margin = m,                   (*right margin, or page width*)
wenzelm@6321
   107
  breakgain = m div 20,         (*minimum added space required of a break*)
wenzelm@6321
   108
  emergencypos = m div 2};      (*position too far to right*)
wenzelm@6116
   109
wenzelm@6321
   110
val margin_info = ref (make_margin_info 76);
wenzelm@6321
   111
fun setmargin m = margin_info := make_margin_info m;
wenzelm@6321
   112
fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
wenzelm@6116
   113
wenzelm@6116
   114
(*Search for the next break (at this or higher levels) and force it to occur*)
wenzelm@6116
   115
fun forcenext [] = []
wenzelm@6116
   116
  | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
wenzelm@6116
   117
  | forcenext (e :: es) = e :: forcenext es;
wenzelm@6116
   118
wenzelm@6116
   119
(*es is list of expressions to print;
wenzelm@6116
   120
  blockin is the indentation of the current block;
wenzelm@6116
   121
  after is the width of the following context until next break. *)
wenzelm@6116
   122
fun format ([], _, _) text = text
wenzelm@6116
   123
  | format (e::es, blockin, after) (text as {pos,nl,...}) =
wenzelm@6116
   124
    (case e of
wenzelm@6116
   125
       Block(bes,indent,wd) =>
wenzelm@6321
   126
         let val blockin' = (pos + indent) mod #emergencypos (! margin_info)
wenzelm@6116
   127
             val btext = format(bes, blockin', breakdist(es,after)) text
wenzelm@6116
   128
             (*If this block was broken then force the next break.*)
wenzelm@6116
   129
             val es2 = if nl < #nl(btext) then forcenext es else es
wenzelm@6116
   130
         in  format (es2,blockin,after) btext  end
wenzelm@6116
   131
     | String (s, len) => format (es,blockin,after) (string s len text)
wenzelm@6116
   132
     | Break(force,wd) => (*no break if text to next break fits on this line
wenzelm@6116
   133
                            or if breaking would add only breakgain to space *)
wenzelm@6116
   134
           format (es,blockin,after)
wenzelm@6116
   135
               (if not force andalso
wenzelm@6321
   136
                   pos+wd <= Int.max(#margin (! margin_info) - breakdist(es,after),
wenzelm@6321
   137
                                     blockin + #breakgain (! margin_info))
wenzelm@6116
   138
                then blanks wd text  (*just insert wd blanks*)
wenzelm@6116
   139
                else blanks blockin (newline text)));
wenzelm@6116
   140
wenzelm@6116
   141
wenzelm@6116
   142
(*** Exported functions to create formatting expressions ***)
wenzelm@6116
   143
wenzelm@6116
   144
fun length (Block (_, _, len)) = len
wenzelm@6116
   145
  | length (String (_, len)) = len
wenzelm@6116
   146
  | length (Break(_, wd)) = wd;
wenzelm@6116
   147
wenzelm@6116
   148
fun str s = String (s, size s);
wenzelm@6116
   149
fun strlen s len = String (s, len);
wenzelm@6321
   150
fun strlen_real s len = strlen s (Real.round len);
wenzelm@6271
   151
val sym = String o apsnd Real.round o Symbol.output_width;
wenzelm@6116
   152
wenzelm@6116
   153
fun spc n = str (repstring " " n);
wenzelm@6116
   154
wenzelm@6116
   155
fun brk wd = Break (false, wd);
wenzelm@6116
   156
val fbrk = Break (true, 0);
wenzelm@6116
   157
wenzelm@6116
   158
fun blk (indent, es) =
wenzelm@6116
   159
  let
wenzelm@6116
   160
    fun sum([], k) = k
wenzelm@6116
   161
      | sum(e :: es, k) = sum (es, length e + k);
wenzelm@6116
   162
  in Block (es, indent, sum (es, 0)) end;
wenzelm@6116
   163
wenzelm@6116
   164
(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
wenzelm@6116
   165
fun lst(lp,rp) es =
wenzelm@6116
   166
  let fun add(e,es) = str"," :: brk 1 :: e :: es;
wenzelm@6116
   167
      fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
wenzelm@6116
   168
        | list(e::[]) = [str lp, e, str rp]
wenzelm@6116
   169
        | list([]) = []
wenzelm@6116
   170
  in blk(size lp, list es) end;
wenzelm@6116
   171
wenzelm@6116
   172
wenzelm@6116
   173
(* utils *)
wenzelm@6116
   174
wenzelm@6116
   175
fun quote prt =
wenzelm@6116
   176
  blk (1, [str "\"", prt, str "\""]);
wenzelm@6116
   177
wenzelm@6116
   178
fun commas prts =
wenzelm@6116
   179
  flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
wenzelm@6116
   180
wenzelm@6116
   181
fun breaks prts = separate (brk 1) prts;
wenzelm@6116
   182
wenzelm@6116
   183
fun fbreaks prts = separate fbrk prts;
wenzelm@6116
   184
wenzelm@6116
   185
fun block prts = blk (2, prts);
wenzelm@6116
   186
wenzelm@6116
   187
val strs = block o breaks o (map str);
wenzelm@6116
   188
wenzelm@6116
   189
fun enclose lpar rpar prts =
wenzelm@6116
   190
  block (str lpar :: (prts @ [str rpar]));
wenzelm@6116
   191
wenzelm@6116
   192
fun list lpar rpar prts =
wenzelm@6116
   193
  enclose lpar rpar (commas prts);
wenzelm@6116
   194
wenzelm@6116
   195
fun str_list lpar rpar strs =
wenzelm@6116
   196
  list lpar rpar (map str strs);
wenzelm@6116
   197
wenzelm@6116
   198
fun big_list name prts =
wenzelm@6116
   199
  block (fbreaks (str name :: prts));
wenzelm@6116
   200
wenzelm@6116
   201
wenzelm@6116
   202
wenzelm@6116
   203
(*** Pretty printing with depth limitation ***)
wenzelm@6116
   204
wenzelm@6116
   205
val depth       = ref 0;        (*maximum depth; 0 means no limit*)
wenzelm@6116
   206
wenzelm@6116
   207
fun setdepth dp = (depth := dp);
wenzelm@6116
   208
wenzelm@6116
   209
(*Recursively prune blocks, discarding all text exceeding depth dp*)
wenzelm@6116
   210
fun pruning dp (Block(bes,indent,wd)) =
wenzelm@6116
   211
      if dp>0 then blk(indent, map (pruning(dp-1)) bes)
wenzelm@6116
   212
              else str "..."
wenzelm@6116
   213
  | pruning dp e = e;
wenzelm@6116
   214
wenzelm@6116
   215
fun prune dp e = if dp>0 then pruning dp e else e;
wenzelm@6116
   216
wenzelm@6116
   217
wenzelm@6321
   218
fun string_of e = #tx (format ([prune (! depth) e], 0, 0) emptytext);
wenzelm@6116
   219
wenzelm@6116
   220
val writeln = writeln o string_of;
wenzelm@6116
   221
wenzelm@6116
   222
wenzelm@6116
   223
(*Create a single flat string: no line breaking*)
wenzelm@6116
   224
fun str_of prt =
wenzelm@6116
   225
  let
wenzelm@6116
   226
    fun s_of (Block (prts, _, _)) = implode (map s_of prts)
wenzelm@6116
   227
      | s_of (String (s, _)) = s
wenzelm@6116
   228
      | s_of (Break (false, wd)) = repstring " " wd
wenzelm@6116
   229
      | s_of (Break (true, _)) = " ";
wenzelm@6321
   230
  in s_of (prune (! depth) prt) end;
wenzelm@6116
   231
wenzelm@6116
   232
(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
wenzelm@6116
   233
fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
wenzelm@6116
   234
  let
wenzelm@6116
   235
    fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
wenzelm@6116
   236
      | pp (String (s, _)) = put_str s
wenzelm@6116
   237
      | pp (Break (false, wd)) = put_brk wd
wenzelm@6116
   238
      | pp (Break (true, _)) = put_fbrk ()
wenzelm@6116
   239
    and pp_lst [] = ()
wenzelm@6116
   240
      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
wenzelm@6116
   241
  in
wenzelm@6116
   242
    pp (prune (! depth) prt)
wenzelm@6116
   243
  end;
wenzelm@6116
   244
wenzelm@6116
   245
wenzelm@6116
   246
end;