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