author | wenzelm |
Sat, 31 Dec 2016 21:00:43 +0100 | |
changeset 64728 | 601866c61ded |
parent 62899 | 845ed4584e21 |
child 67522 | 9e712280cc37 |
permissions | -rw-r--r-- |
6118 | 1 |
(* Title: Pure/General/pretty.ML |
8806 | 2 |
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
|
3 |
Author: Markus Wenzel, TU Munich |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
4 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
5 |
Generic pretty printing module. |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
6 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
7 |
Loosely based on |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
8 |
D. C. Oppen, "Pretty Printing", |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
9 |
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
|
10 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
11 |
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
|
12 |
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
|
13 |
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
|
14 |
text is indented to the level of the enclosing block. Normally, if a block |
61864 | 15 |
is broken then all enclosing blocks will also be broken. |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
16 |
|
61864 | 17 |
The stored length of a block is used in break_dist (to treat each inner block as |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
18 |
a unit for breaking). |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
19 |
*) |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
20 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
21 |
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
|
22 |
sig |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
23 |
val default_indent: string -> int -> Output.output |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
24 |
val add_mode: string -> (string -> int -> Output.output) -> unit |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
25 |
type T |
62783 | 26 |
val make_block: {markup: Output.output * Output.output, consistent: bool, indent: int} -> |
27 |
T list -> T |
|
28 |
val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
29 |
val str: string -> T |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
30 |
val brk: int -> T |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
56334
diff
changeset
|
31 |
val brk_indent: int -> int -> T |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
32 |
val fbrk: T |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
33 |
val breaks: T list -> T list |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
34 |
val fbreaks: T list -> T list |
23645 | 35 |
val blk: int * T list -> T |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
36 |
val block: T list -> T |
23645 | 37 |
val strs: string list -> T |
23617 | 38 |
val markup: Markup.T -> T list -> T |
26703 | 39 |
val mark: Markup.T -> T -> T |
42266 | 40 |
val mark_str: Markup.T * string -> T |
41 |
val marks_str: Markup.T list * string -> T |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51511
diff
changeset
|
42 |
val item: T list -> T |
52693 | 43 |
val text_fold: T list -> T |
55763 | 44 |
val keyword1: string -> T |
45 |
val keyword2: string -> T |
|
50162 | 46 |
val text: string -> T list |
47 |
val paragraph: T list -> T |
|
48 |
val para: string -> T |
|
18802 | 49 |
val quote: T -> T |
55033 | 50 |
val cartouche: T -> T |
18802 | 51 |
val separate: string -> T list -> T list |
52 |
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
|
53 |
val enclose: string -> string -> T list -> T |
18802 | 54 |
val enum: string -> string -> string -> T list -> T |
30620 | 55 |
val position: Position.T -> T |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
val big_list: string -> T list -> T |
9730 | 59 |
val indent: int -> T -> T |
23645 | 60 |
val unbreakable: T -> T |
36745 | 61 |
val margin_default: int Unsynchronized.ref |
23645 | 62 |
val symbolicN: string |
36745 | 63 |
val output_buffer: int option -> T -> Buffer.T |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
64 |
val output: int option -> T -> Output.output |
36745 | 65 |
val string_of_margin: int -> T -> string |
23645 | 66 |
val string_of: T -> string |
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
67 |
val writeln: T -> unit |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
68 |
val symbolic_output: T -> Output.output |
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49554
diff
changeset
|
69 |
val symbolic_string_of: T -> string |
61877
276ad4354069
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents:
61870
diff
changeset
|
70 |
val unformatted_string_of: T -> string |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
71 |
val markup_chunks: Markup.T -> T list -> T |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
72 |
val chunks: T list -> T |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
73 |
val chunks2: T list -> T |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
74 |
val block_enclose: T * T -> T list -> T |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
75 |
val writeln_chunks: T list -> unit |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
76 |
val writeln_chunks2: T list -> unit |
62784
0371c369ab1d
adapted to Poly/ML repository version 2e40cadc975a;
wenzelm
parents:
62783
diff
changeset
|
77 |
val to_ML: FixedInt.int -> T -> ML_Pretty.pretty |
36748 | 78 |
val from_ML: ML_Pretty.pretty -> T |
62823 | 79 |
val to_polyml: T -> PolyML_Pretty.pretty |
80 |
val from_polyml: PolyML_Pretty.pretty -> 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
|
81 |
end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
82 |
|
23617 | 83 |
structure Pretty: PRETTY = |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
84 |
struct |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
85 |
|
23617 | 86 |
(** print mode operations **) |
87 |
||
61865 | 88 |
fun default_indent (_: string) = Symbol.spaces; |
23617 | 89 |
|
90 |
local |
|
23698 | 91 |
val default = {indent = default_indent}; |
43684 | 92 |
val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]); |
23617 | 93 |
in |
43684 | 94 |
fun add_mode name indent = |
46894
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45666
diff
changeset
|
95 |
Synchronized.change modes (fn tab => |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45666
diff
changeset
|
96 |
(if not (Symtab.defined tab name) then () |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45666
diff
changeset
|
97 |
else warning ("Redefining pretty mode " ^ quote name); |
e2ad717ec889
allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents:
45666
diff
changeset
|
98 |
Symtab.update (name, {indent = indent}) tab)); |
23617 | 99 |
fun get_mode () = |
43684 | 100 |
the_default default |
101 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
|
23617 | 102 |
end; |
103 |
||
104 |
fun mode_indent x y = #indent (get_mode ()) x y; |
|
23645 | 105 |
|
61865 | 106 |
val output_spaces = Output.output o Symbol.spaces; |
23645 | 107 |
val add_indent = Buffer.add o output_spaces; |
23617 | 108 |
|
109 |
||
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
110 |
|
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
111 |
(** printing items: compound phrases, strings, and breaks **) |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
112 |
|
62785
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
113 |
val force_nat = Integer.max 0; |
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
114 |
|
37529 | 115 |
abstype T = |
61869 | 116 |
Block of (Output.output * Output.output) * bool * int * T list * int |
117 |
(*markup output, consistent, indentation, body, length*) |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
56334
diff
changeset
|
118 |
| Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*) |
61870 | 119 |
| Str of Output.output * int (*text, length*) |
37529 | 120 |
with |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
121 |
|
61864 | 122 |
fun length (Block (_, _, _, _, len)) = len |
61870 | 123 |
| length (Break (_, wd, _)) = wd |
124 |
| length (Str (_, len)) = len; |
|
23645 | 125 |
|
62783 | 126 |
fun make_block {markup, consistent, indent} body = |
61883
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
127 |
let |
62785
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
128 |
val indent' = force_nat indent; |
61883
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
129 |
fun body_length prts len = |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
130 |
let |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
131 |
val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts; |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
132 |
val len' = Int.max (fold (Integer.add o length) line 0, len); |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
133 |
in |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
134 |
(case rest of |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
135 |
Break (true, _, ind) :: rest' => |
62785
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
136 |
body_length (Break (false, indent' + ind, 0) :: rest') len' |
61883
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
137 |
| [] => len') |
c0f34fe6aa61
clarified length of block with pre-existant forced breaks;
wenzelm
parents:
61877
diff
changeset
|
138 |
end; |
62785
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
139 |
in Block (markup, consistent, indent', body, body_length body 0) end; |
61864 | 140 |
|
62783 | 141 |
fun markup_block {markup, consistent, indent} es = |
142 |
make_block {markup = Markup.output markup, consistent = consistent, indent = indent} es; |
|
61864 | 143 |
|
9730 | 144 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
145 |
|
23645 | 146 |
(** derived operations to create formatting expressions **) |
147 |
||
62785
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
148 |
val str = Output.output_width ##> force_nat #> Str; |
23645 | 149 |
|
62785
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
150 |
fun brk wd = Break (false, force_nat wd, 0); |
70b9c7d4ed7f
more robust pretty printing: permissive treatment of bad values;
wenzelm
parents:
62784
diff
changeset
|
151 |
fun brk_indent wd ind = Break (false, force_nat wd, ind); |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
56334
diff
changeset
|
152 |
val fbrk = Break (true, 1, 0); |
23645 | 153 |
|
154 |
fun breaks prts = Library.separate (brk 1) prts; |
|
155 |
fun fbreaks prts = Library.separate fbrk prts; |
|
156 |
||
62783 | 157 |
fun blk (indent, es) = |
158 |
markup_block {markup = Markup.empty, consistent = false, indent = indent} es; |
|
159 |
||
23645 | 160 |
fun block prts = blk (2, prts); |
161 |
val strs = block o breaks o map str; |
|
162 |
||
62783 | 163 |
fun markup m = markup_block {markup = m, consistent = false, indent = 0}; |
42266 | 164 |
fun mark m prt = if m = Markup.empty then prt else markup m [prt]; |
165 |
fun mark_str (m, s) = mark m (str s); |
|
166 |
fun marks_str (ms, s) = fold_rev mark ms (str s); |
|
167 |
||
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51511
diff
changeset
|
168 |
val item = markup Markup.item; |
52693 | 169 |
val text_fold = markup Markup.text_fold; |
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
51511
diff
changeset
|
170 |
|
55763 | 171 |
fun keyword1 name = mark_str (Markup.keyword1, name); |
172 |
fun keyword2 name = mark_str (Markup.keyword2, name); |
|
23645 | 173 |
|
50162 | 174 |
val text = breaks o map str o Symbol.explode_words; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50162
diff
changeset
|
175 |
val paragraph = markup Markup.paragraph; |
50162 | 176 |
val para = paragraph o text; |
177 |
||
23645 | 178 |
fun quote prt = blk (1, [str "\"", prt, str "\""]); |
62210 | 179 |
fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]); |
23645 | 180 |
|
181 |
fun separate sep prts = |
|
182 |
flat (Library.separate [str sep, brk 1] (map single prts)); |
|
183 |
||
184 |
val commas = separate ","; |
|
185 |
||
186 |
fun enclose lpar rpar prts = |
|
187 |
block (str lpar :: (prts @ [str rpar])); |
|
188 |
||
189 |
fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts); |
|
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
190 |
|
30620 | 191 |
val position = |
192 |
enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of; |
|
193 |
||
23645 | 194 |
val list = enum ","; |
195 |
fun str_list lpar rpar strs = list lpar rpar (map str strs); |
|
196 |
||
197 |
fun big_list name prts = block (fbreaks (str name :: prts)); |
|
198 |
||
199 |
fun indent 0 prt = prt |
|
61865 | 200 |
| indent n prt = blk (0, [str (Symbol.spaces n), prt]); |
23645 | 201 |
|
61870 | 202 |
fun unbreakable (Block (m, consistent, indent, es, len)) = |
61869 | 203 |
Block (m, consistent, indent, map unbreakable es, len) |
61870 | 204 |
| unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd) |
205 |
| unbreakable (e as Str _) = e; |
|
23645 | 206 |
|
207 |
||
208 |
||
209 |
(** formatting **) |
|
210 |
||
211 |
(* formatted output *) |
|
212 |
||
213 |
local |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
214 |
|
17756 | 215 |
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int}; |
216 |
||
217 |
val empty: text = |
|
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
218 |
{tx = Buffer.empty, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
219 |
ind = Buffer.empty, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
220 |
pos = 0, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
221 |
nl = 0}; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
222 |
|
32784 | 223 |
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
|
224 |
{tx = Buffer.add (Output.output "\n") tx, |
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
225 |
ind = Buffer.empty, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
226 |
pos = 0, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
227 |
nl = nl + 1}; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
228 |
|
23628
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
229 |
fun control s {tx, ind, pos: int, nl} : text = |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
230 |
{tx = Buffer.add s tx, |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
231 |
ind = ind, |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
232 |
pos = pos, |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
233 |
nl = nl}; |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
234 |
|
17756 | 235 |
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
|
236 |
{tx = Buffer.add s tx, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
237 |
ind = Buffer.add s ind, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
238 |
pos = pos + len, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
239 |
nl = nl}; |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
240 |
|
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
241 |
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
|
242 |
|
17756 | 243 |
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
|
244 |
let val s = Buffer.content buf in |
23617 | 245 |
{tx = Buffer.add (mode_indent s len) tx, |
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
246 |
ind = Buffer.add s ind, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
247 |
pos = pos + len, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
248 |
nl = nl} |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
249 |
end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
250 |
|
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
251 |
(*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
|
252 |
include "after", to account for text following this block.*) |
61864 | 253 |
fun break_dist (Break _ :: _, _) = 0 |
61870 | 254 |
| break_dist (e :: es, after) = length e + break_dist (es, after) |
61864 | 255 |
| break_dist ([], after) = after; |
256 |
||
257 |
val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e; |
|
258 |
val force_all = map force_break; |
|
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
259 |
|
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
260 |
(*Search for the next break (at this or higher levels) and force it to occur.*) |
61864 | 261 |
fun force_next [] = [] |
262 |
| force_next ((e as Break _) :: es) = force_break e :: es |
|
263 |
| force_next (e :: es) = e :: force_next es; |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
264 |
|
23645 | 265 |
in |
19266 | 266 |
|
36745 | 267 |
fun formatted margin input = |
268 |
let |
|
269 |
val breakgain = margin div 20; (*minimum added space required of a break*) |
|
270 |
val emergencypos = margin div 2; (*position too far to right*) |
|
271 |
||
272 |
(*es is list of expressions to print; |
|
273 |
blockin is the indentation of the current block; |
|
274 |
after is the width of the following context until next break.*) |
|
275 |
fun format ([], _, _) text = text |
|
276 |
| format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) = |
|
277 |
(case e of |
|
61869 | 278 |
Block ((bg, en), consistent, indent, bes, blen) => |
36745 | 279 |
let |
280 |
val pos' = pos + indent; |
|
281 |
val pos'' = pos' mod emergencypos; |
|
282 |
val block' = |
|
283 |
if pos' < emergencypos then (ind |> add_indent indent, pos') |
|
284 |
else (add_indent pos'' Buffer.empty, pos''); |
|
61864 | 285 |
val d = break_dist (es, after) |
286 |
val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes; |
|
36745 | 287 |
val btext: text = text |
288 |
|> control bg |
|
61864 | 289 |
|> format (bes', block', d) |
36745 | 290 |
|> control en; |
291 |
(*if this block was broken then force the next break*) |
|
61864 | 292 |
val es' = if nl < #nl btext then force_next es else es; |
36745 | 293 |
in format (es', block, after) btext end |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
56334
diff
changeset
|
294 |
| Break (force, wd, ind) => |
36745 | 295 |
(*no break if text to next break fits on this line |
296 |
or if breaking would add only breakgain to space*) |
|
297 |
format (es, block, after) |
|
298 |
(if not force andalso |
|
61864 | 299 |
pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain) |
300 |
then text |> blanks wd (*just insert wd blanks*) |
|
301 |
else text |> newline |> indentation block |> blanks ind) |
|
61870 | 302 |
| Str str => format (es, block, after) (string str text)); |
36745 | 303 |
in |
36747
7361d5dde9ce
discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
wenzelm
parents:
36745
diff
changeset
|
304 |
#tx (format ([input], (Buffer.empty, 0), 0) empty) |
36745 | 305 |
end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
306 |
|
23645 | 307 |
end; |
14832
6589a58f57cb
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents:
12421
diff
changeset
|
308 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
309 |
|
23645 | 310 |
(* special output *) |
18802 | 311 |
|
23645 | 312 |
(*symbolic markup -- no formatting*) |
313 |
fun symbolic prt = |
|
314 |
let |
|
61869 | 315 |
fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en |
316 |
| out (Block ((bg, en), consistent, indent, prts, _)) = |
|
45666 | 317 |
Buffer.add bg #> |
61864 | 318 |
Buffer.markup (Markup.block consistent indent) (fold out prts) #> |
45666 | 319 |
Buffer.add en |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
56334
diff
changeset
|
320 |
| out (Break (false, wd, ind)) = |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
56334
diff
changeset
|
321 |
Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd)) |
61870 | 322 |
| out (Break (true, _, _)) = Buffer.add (Output.output "\n") |
323 |
| out (Str (s, _)) = Buffer.add s; |
|
23645 | 324 |
in out prt Buffer.empty end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
325 |
|
23645 | 326 |
(*unformatted output*) |
327 |
fun unformatted prt = |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
328 |
let |
61869 | 329 |
fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en |
61870 | 330 |
| fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd) |
331 |
| fmt (Str (s, _)) = Buffer.add s; |
|
36747
7361d5dde9ce
discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
wenzelm
parents:
36745
diff
changeset
|
332 |
in fmt prt Buffer.empty end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
333 |
|
30624
e755b8b76365
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30620
diff
changeset
|
334 |
|
36748 | 335 |
(* output interfaces *) |
30620 | 336 |
|
62899
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
337 |
val margin_default = Unsynchronized.ref ML_Pretty.default_margin; (*right margin, or page width*) |
23645 | 338 |
|
339 |
val symbolicN = "pretty_symbolic"; |
|
340 |
||
36745 | 341 |
fun output_buffer margin prt = |
23645 | 342 |
if print_mode_active symbolicN then symbolic prt |
36745 | 343 |
else formatted (the_default (! margin_default) margin) prt; |
23645 | 344 |
|
36745 | 345 |
val output = Buffer.content oo output_buffer; |
346 |
fun string_of_margin margin = Output.escape o output (SOME margin); |
|
347 |
val string_of = Output.escape o output NONE; |
|
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
348 |
val writeln = Output.writeln o string_of; |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
349 |
|
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
350 |
val symbolic_output = Buffer.content o symbolic; |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
351 |
val symbolic_string_of = Output.escape o symbolic_output; |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
352 |
|
61877
276ad4354069
renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents:
61870
diff
changeset
|
353 |
val unformatted_string_of = Output.escape o Buffer.content o unformatted; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
354 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
355 |
|
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
356 |
(* chunks *) |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
357 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
358 |
fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts)); |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
359 |
val chunks = markup_chunks Markup.empty; |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
360 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
361 |
fun chunks2 prts = |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
362 |
(case try split_last prts of |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
363 |
NONE => blk (0, []) |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
364 |
| SOME (prefix, last) => |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
365 |
blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]])); |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
366 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
367 |
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2]; |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
368 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
369 |
fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold; |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
370 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
371 |
fun writeln_chunks prts = |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
372 |
Output.writelns (Library.separate "\n" (map string_of_text_fold prts)); |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
373 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
374 |
fun writeln_chunks2 prts = |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
375 |
(case try split_last prts of |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
376 |
NONE => () |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
377 |
| SOME (prefix, last) => |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
378 |
(map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @ |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
379 |
[string_of_text_fold last]) |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
380 |
|> Output.writelns); |
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
381 |
|
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
55918
diff
changeset
|
382 |
|
14832
6589a58f57cb
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents:
12421
diff
changeset
|
383 |
|
62663 | 384 |
(** toplevel pretty printing **) |
36748 | 385 |
|
62667 | 386 |
fun to_ML 0 (Block _) = ML_Pretty.str "..." |
387 |
| to_ML depth (Block (m, consistent, indent, prts, _)) = |
|
388 |
ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map (to_ML (depth - 1)) prts) |
|
389 |
| to_ML _ (Break (force, wd, ind)) = |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62210
diff
changeset
|
390 |
ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind) |
62667 | 391 |
| to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len); |
36748 | 392 |
|
61869 | 393 |
fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) = |
62783 | 394 |
make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent} |
395 |
(map from_ML prts) |
|
62387
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62210
diff
changeset
|
396 |
| from_ML (ML_Pretty.Break (force, wd, ind)) = |
ad3eb2889f9a
support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents:
62210
diff
changeset
|
397 |
Break (force, FixedInt.toInt wd, FixedInt.toInt ind) |
62820 | 398 |
| from_ML (ML_Pretty.String (s, len)) = Str (s, force_nat (FixedInt.toInt len)); |
36748 | 399 |
|
62667 | 400 |
val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml; |
62663 | 401 |
val from_polyml = ML_Pretty.from_polyml #> from_ML; |
402 |
||
37529 | 403 |
end; |
404 |
||
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62785
diff
changeset
|
405 |
val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote); |
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62785
diff
changeset
|
406 |
val _ = ML_system_pp (fn _ => fn _ => to_polyml o position); |
62663 | 407 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
408 |
end; |
62899
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
409 |
|
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
410 |
structure ML_Pretty = |
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
411 |
struct |
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
412 |
open ML_Pretty; |
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
413 |
val string_of_polyml = Pretty.string_of o Pretty.from_polyml; |
845ed4584e21
clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents:
62823
diff
changeset
|
414 |
end; |