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