author | wenzelm |
Thu, 22 Nov 2012 12:22:03 +0100 | |
changeset 50162 | e06eabc421e7 |
parent 49656 | 7ff712de5747 |
child 50201 | c26369c9eda6 |
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 |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
15 |
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
|
16 |
breaks" are provided. |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
17 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
18 |
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
|
19 |
a unit for breaking). |
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 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
22 |
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
|
23 |
sig |
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
24 |
val spaces: int -> string |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
type T |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
28 |
val str: string -> T |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
29 |
val brk: int -> T |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
30 |
val fbrk: T |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
31 |
val breaks: T list -> T list |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
32 |
val fbreaks: T list -> T list |
23645 | 33 |
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
|
34 |
val block: T list -> T |
23645 | 35 |
val strs: string list -> T |
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
36 |
val raw_markup: Output.output * Output.output -> int * T list -> T |
23617 | 37 |
val markup: Markup.T -> T list -> T |
26703 | 38 |
val mark: Markup.T -> T -> T |
42266 | 39 |
val mark_str: Markup.T * string -> T |
40 |
val marks_str: Markup.T list * string -> T |
|
49554
7b7bd2d7661d
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
wenzelm
parents:
48704
diff
changeset
|
41 |
val command: string -> T |
23617 | 42 |
val keyword: string -> T |
50162 | 43 |
val text: string -> T list |
44 |
val paragraph: T list -> T |
|
45 |
val para: string -> T |
|
23638 | 46 |
val markup_chunks: Markup.T -> T list -> T |
18802 | 47 |
val chunks: T list -> T |
19266 | 48 |
val chunks2: T list -> T |
23617 | 49 |
val block_enclose: T * T -> T list -> T |
18802 | 50 |
val quote: T -> T |
51 |
val backquote: T -> T |
|
52 |
val separate: string -> T list -> T list |
|
53 |
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
|
54 |
val enclose: string -> string -> T list -> T |
18802 | 55 |
val enum: string -> string -> string -> T list -> T |
30620 | 56 |
val position: Position.T -> T |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
val big_list: string -> T list -> T |
9730 | 60 |
val indent: int -> T -> T |
23645 | 61 |
val unbreakable: T -> T |
36745 | 62 |
val margin_default: int Unsynchronized.ref |
23645 | 63 |
val symbolicN: string |
36745 | 64 |
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
|
65 |
val output: int option -> T -> Output.output |
36745 | 66 |
val string_of_margin: int -> T -> string |
23645 | 67 |
val string_of: T -> string |
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
68 |
val writeln: T -> unit |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
69 |
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
|
70 |
val symbolic_string_of: T -> string |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
71 |
val str_of: T -> string |
36748 | 72 |
val to_ML: T -> ML_Pretty.pretty |
73 |
val from_ML: ML_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
|
74 |
end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
75 |
|
23617 | 76 |
structure Pretty: PRETTY = |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
77 |
struct |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
78 |
|
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
79 |
(** spaces **) |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
80 |
|
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
81 |
local |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
82 |
val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space); |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
83 |
in |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
84 |
fun spaces k = |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
85 |
if k < 64 then Vector.sub (small_spaces, k) |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
86 |
else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^ |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
87 |
Vector.sub (small_spaces, k mod 64); |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
88 |
end; |
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
89 |
|
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
90 |
|
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
91 |
|
23617 | 92 |
(** print mode operations **) |
93 |
||
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
94 |
fun default_indent (_: string) = spaces; |
23617 | 95 |
|
96 |
local |
|
23698 | 97 |
val default = {indent = default_indent}; |
43684 | 98 |
val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]); |
23617 | 99 |
in |
43684 | 100 |
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
|
101 |
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
|
102 |
(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
|
103 |
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
|
104 |
Symtab.update (name, {indent = indent}) tab)); |
23617 | 105 |
fun get_mode () = |
43684 | 106 |
the_default default |
107 |
(Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
|
23617 | 108 |
end; |
109 |
||
110 |
fun mode_indent x y = #indent (get_mode ()) x y; |
|
23645 | 111 |
|
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
112 |
val output_spaces = Output.output o spaces; |
23645 | 113 |
val add_indent = Buffer.add o output_spaces; |
23617 | 114 |
|
115 |
||
10952
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 |
(** printing items: compound phrases, strings, and breaks **) |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
118 |
|
37529 | 119 |
abstype T = |
40131
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
120 |
Block of (Output.output * Output.output) * T list * int * int |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
121 |
(*markup output, body, indentation, length*) |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
122 |
| String of Output.output * int (*text, length*) |
7cbebd636e79
explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents:
38474
diff
changeset
|
123 |
| Break of bool * int (*mandatory flag, width if not taken*) |
37529 | 124 |
with |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
125 |
|
23645 | 126 |
fun length (Block (_, _, _, len)) = len |
127 |
| length (String (_, len)) = len |
|
128 |
| length (Break (_, wd)) = wd; |
|
129 |
||
9730 | 130 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
131 |
|
23645 | 132 |
(** derived operations to create formatting expressions **) |
133 |
||
134 |
val str = String o Output.output_width; |
|
135 |
||
136 |
fun brk wd = Break (false, wd); |
|
36690
97d2780ad6f0
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
wenzelm
parents:
36689
diff
changeset
|
137 |
val fbrk = Break (true, 1); |
23645 | 138 |
|
139 |
fun breaks prts = Library.separate (brk 1) prts; |
|
140 |
fun fbreaks prts = Library.separate fbrk prts; |
|
141 |
||
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
142 |
fun raw_markup m (indent, es) = |
23645 | 143 |
let |
144 |
fun sum [] k = k |
|
145 |
| sum (e :: es) k = sum es (length e + k); |
|
146 |
in Block (m, es, indent, sum es 0) end; |
|
147 |
||
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
148 |
fun markup_block m arg = raw_markup (Markup.output m) arg; |
30667
53fbf7c679b0
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
wenzelm
parents:
30624
diff
changeset
|
149 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
37529
diff
changeset
|
150 |
val blk = markup_block Markup.empty; |
23645 | 151 |
fun block prts = blk (2, prts); |
152 |
val strs = block o breaks o map str; |
|
153 |
||
154 |
fun markup m prts = markup_block m (0, prts); |
|
42266 | 155 |
fun mark m prt = if m = Markup.empty then prt else markup m [prt]; |
156 |
fun mark_str (m, s) = mark m (str s); |
|
157 |
fun marks_str (ms, s) = fold_rev mark ms (str s); |
|
158 |
||
49554
7b7bd2d7661d
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
wenzelm
parents:
48704
diff
changeset
|
159 |
fun command name = mark_str (Isabelle_Markup.keyword1, name); |
7b7bd2d7661d
more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;
wenzelm
parents:
48704
diff
changeset
|
160 |
fun keyword name = mark_str (Isabelle_Markup.keyword2, name); |
23645 | 161 |
|
50162 | 162 |
val text = breaks o map str o Symbol.explode_words; |
163 |
val paragraph = markup Isabelle_Markup.paragraph; |
|
164 |
val para = paragraph o text; |
|
165 |
||
23645 | 166 |
fun markup_chunks m prts = markup m (fbreaks prts); |
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
37529
diff
changeset
|
167 |
val chunks = markup_chunks Markup.empty; |
23645 | 168 |
fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts))); |
169 |
||
36733 | 170 |
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2]; |
23645 | 171 |
|
172 |
fun quote prt = blk (1, [str "\"", prt, str "\""]); |
|
173 |
fun backquote prt = blk (1, [str "`", prt, str "`"]); |
|
174 |
||
175 |
fun separate sep prts = |
|
176 |
flat (Library.separate [str sep, brk 1] (map single prts)); |
|
177 |
||
178 |
val commas = separate ","; |
|
179 |
||
180 |
fun enclose lpar rpar prts = |
|
181 |
block (str lpar :: (prts @ [str rpar])); |
|
182 |
||
183 |
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
|
184 |
|
30620 | 185 |
val position = |
186 |
enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of; |
|
187 |
||
23645 | 188 |
val list = enum ","; |
189 |
fun str_list lpar rpar strs = list lpar rpar (map str strs); |
|
190 |
||
191 |
fun big_list name prts = block (fbreaks (str name :: prts)); |
|
192 |
||
193 |
fun indent 0 prt = prt |
|
48704
85a3de10567d
tuned signature -- make Pretty less dependent on Symbol;
wenzelm
parents:
46894
diff
changeset
|
194 |
| indent n prt = blk (0, [str (spaces n), prt]); |
23645 | 195 |
|
196 |
fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd) |
|
197 |
| unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd) |
|
198 |
| unbreakable (e as String _) = e; |
|
199 |
||
200 |
||
201 |
||
202 |
(** formatting **) |
|
203 |
||
204 |
(* formatted output *) |
|
205 |
||
206 |
local |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
207 |
|
17756 | 208 |
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int}; |
209 |
||
210 |
val empty: text = |
|
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
211 |
{tx = Buffer.empty, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
212 |
ind = Buffer.empty, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
213 |
pos = 0, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
214 |
nl = 0}; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
215 |
|
32784 | 216 |
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
|
217 |
{tx = Buffer.add (Output.output "\n") tx, |
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
218 |
ind = Buffer.empty, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
219 |
pos = 0, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
220 |
nl = nl + 1}; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
221 |
|
23628
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
222 |
fun control s {tx, ind, pos: int, nl} : text = |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
223 |
{tx = Buffer.add s tx, |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
224 |
ind = ind, |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
225 |
pos = pos, |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
226 |
nl = nl}; |
41cdbfb9f77b
markup: emit as control information -- no indent text;
wenzelm
parents:
23617
diff
changeset
|
227 |
|
17756 | 228 |
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
|
229 |
{tx = Buffer.add s tx, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
230 |
ind = Buffer.add s ind, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
231 |
pos = pos + len, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
232 |
nl = nl}; |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
233 |
|
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
234 |
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
|
235 |
|
17756 | 236 |
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
|
237 |
let val s = Buffer.content buf in |
23617 | 238 |
{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
|
239 |
ind = Buffer.add s ind, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
240 |
pos = pos + len, |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
241 |
nl = nl} |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
242 |
end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
243 |
|
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
244 |
(*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
|
245 |
include "after", to account for text following this block.*) |
36687 | 246 |
fun breakdist (Break _ :: _, _) = 0 |
247 |
| breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after) |
|
32784 | 248 |
| breakdist (String (_, len) :: es, after) = len + breakdist (es, after) |
10952
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
249 |
| breakdist ([], after) = after; |
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
250 |
|
b520e4f1313b
support general indentation (e.g. for non-tt latex output);
wenzelm
parents:
9730
diff
changeset
|
251 |
(*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
|
252 |
fun forcenext [] = [] |
36690
97d2780ad6f0
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
wenzelm
parents:
36689
diff
changeset
|
253 |
| forcenext (Break _ :: es) = fbrk :: es |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
254 |
| forcenext (e :: es) = e :: forcenext es; |
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
255 |
|
23645 | 256 |
in |
19266 | 257 |
|
36745 | 258 |
fun formatted margin input = |
259 |
let |
|
260 |
val breakgain = margin div 20; (*minimum added space required of a break*) |
|
261 |
val emergencypos = margin div 2; (*position too far to right*) |
|
262 |
||
263 |
(*es is list of expressions to print; |
|
264 |
blockin is the indentation of the current block; |
|
265 |
after is the width of the following context until next break.*) |
|
266 |
fun format ([], _, _) text = text |
|
267 |
| format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) = |
|
268 |
(case e of |
|
269 |
Block ((bg, en), bes, indent, _) => |
|
270 |
let |
|
271 |
val pos' = pos + indent; |
|
272 |
val pos'' = pos' mod emergencypos; |
|
273 |
val block' = |
|
274 |
if pos' < emergencypos then (ind |> add_indent indent, pos') |
|
275 |
else (add_indent pos'' Buffer.empty, pos''); |
|
276 |
val btext: text = text |
|
277 |
|> control bg |
|
278 |
|> format (bes, block', breakdist (es, after)) |
|
279 |
|> control en; |
|
280 |
(*if this block was broken then force the next break*) |
|
281 |
val es' = if nl < #nl btext then forcenext es else es; |
|
282 |
in format (es', block, after) btext end |
|
283 |
| Break (force, wd) => |
|
284 |
(*no break if text to next break fits on this line |
|
285 |
or if breaking would add only breakgain to space*) |
|
286 |
format (es, block, after) |
|
287 |
(if not force andalso |
|
288 |
pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain) |
|
289 |
then text |> blanks wd (*just insert wd blanks*) |
|
290 |
else text |> newline |> indentation block) |
|
291 |
| String str => format (es, block, after) (string str text)); |
|
292 |
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
|
293 |
#tx (format ([input], (Buffer.empty, 0), 0) empty) |
36745 | 294 |
end; |
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
295 |
|
23645 | 296 |
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
|
297 |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
298 |
|
23645 | 299 |
(* special output *) |
18802 | 300 |
|
23645 | 301 |
(*symbolic markup -- no formatting*) |
302 |
fun symbolic prt = |
|
303 |
let |
|
30667
53fbf7c679b0
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
wenzelm
parents:
30624
diff
changeset
|
304 |
fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en |
53fbf7c679b0
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
wenzelm
parents:
30624
diff
changeset
|
305 |
| out (Block ((bg, en), prts, indent, _)) = |
45666 | 306 |
Buffer.add bg #> |
307 |
Buffer.markup (Isabelle_Markup.block indent) (fold out prts) #> |
|
308 |
Buffer.add en |
|
23645 | 309 |
| out (String (s, _)) = Buffer.add s |
45666 | 310 |
| out (Break (false, wd)) = |
311 |
Buffer.markup (Isabelle_Markup.break wd) (Buffer.add (output_spaces wd)) |
|
36689
379f5b1e7f91
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;
wenzelm
parents:
36687
diff
changeset
|
312 |
| out (Break (true, _)) = Buffer.add (Output.output "\n"); |
23645 | 313 |
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
|
314 |
|
23645 | 315 |
(*unformatted output*) |
316 |
fun unformatted prt = |
|
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
317 |
let |
30667
53fbf7c679b0
Block markup: maintain output version within tree values (in accordance with String) -- changes operational behaviour wrt. print_mode;
wenzelm
parents:
30624
diff
changeset
|
318 |
fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en |
23617 | 319 |
| fmt (String (s, _)) = Buffer.add s |
36690
97d2780ad6f0
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;
wenzelm
parents:
36689
diff
changeset
|
320 |
| fmt (Break (_, wd)) = Buffer.add (output_spaces wd); |
36747
7361d5dde9ce
discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
wenzelm
parents:
36745
diff
changeset
|
321 |
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
|
322 |
|
30624
e755b8b76365
simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents:
30620
diff
changeset
|
323 |
|
36748 | 324 |
(* output interfaces *) |
30620 | 325 |
|
36748 | 326 |
val margin_default = Unsynchronized.ref 76; (*right margin, or page width*) |
23645 | 327 |
|
328 |
val symbolicN = "pretty_symbolic"; |
|
329 |
||
36745 | 330 |
fun output_buffer margin prt = |
23645 | 331 |
if print_mode_active symbolicN then symbolic prt |
36745 | 332 |
else formatted (the_default (! margin_default) margin) prt; |
23645 | 333 |
|
36745 | 334 |
val output = Buffer.content oo output_buffer; |
335 |
fun string_of_margin margin = Output.escape o output (SOME margin); |
|
336 |
val string_of = Output.escape o output NONE; |
|
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
337 |
val writeln = Output.writeln o string_of; |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
338 |
|
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
339 |
val symbolic_output = Buffer.content o symbolic; |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
340 |
val symbolic_string_of = Output.escape o symbolic_output; |
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
341 |
|
23645 | 342 |
val str_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
|
343 |
|
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
344 |
|
14832
6589a58f57cb
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents:
12421
diff
changeset
|
345 |
|
36748 | 346 |
(** ML toplevel pretty printing **) |
347 |
||
348 |
fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind) |
|
349 |
| to_ML (String s) = ML_Pretty.String s |
|
350 |
| to_ML (Break b) = ML_Pretty.Break b; |
|
351 |
||
49656
7ff712de5747
treat wrapped markup elements as raw markup delimiters;
wenzelm
parents:
49565
diff
changeset
|
352 |
fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts) |
36748 | 353 |
| from_ML (ML_Pretty.String s) = String s |
354 |
| from_ML (ML_Pretty.Break b) = Break b; |
|
355 |
||
37529 | 356 |
end; |
357 |
||
6116
8ba2f25610f7
files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff
changeset
|
358 |
end; |