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