--- a/src/Pure/General/pretty.ML Sun Jul 08 13:10:51 2007 +0200
+++ b/src/Pure/General/pretty.ML Sun Jul 08 13:10:54 2007 +0200
@@ -27,21 +27,21 @@
sig
val default_indent: string -> int -> string
val default_markup: Markup.T -> string * string
+ val mode_markup: Markup.T -> string * string
val add_mode: string -> (string -> int -> string) -> (Markup.T -> string * string) -> unit
type T
val raw_str: string * int -> T
val str: string -> T
val brk: int -> T
val fbrk: T
- val blk: int * T list -> T
- val unbreakable: T -> T
val breaks: T list -> T list
val fbreaks: T list -> T list
+ val blk: int * T list -> T
val block: T list -> T
+ val strs: string list -> T
val markup: Markup.T -> T list -> T
val keyword: string -> T
val command: string -> T
- val strs: string list -> T
val markup_chunks: Markup.T -> T list -> T
val chunks: T list -> T
val chunks2: T list -> T
@@ -56,15 +56,17 @@
val str_list: string -> string -> string list -> T
val big_list: string -> T list -> T
val indent: int -> T -> T
- val string_of: T -> string
+ val unbreakable: T -> T
+ val setmargin: int -> unit
+ val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
+ val setdepth: int -> unit
+ val pprint: T -> pprint_args -> unit
+ val symbolicN: string
val output_buffer: T -> Buffer.T
val output: T -> string
- val writeln: T -> unit
+ val string_of: T -> string
val str_of: T -> string
- val pprint: T -> pprint_args -> unit
- val setdepth: int -> unit
- val setmargin: int -> unit
- val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
+ val writeln: T -> unit
type pp
val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
val term: pp -> term -> T
@@ -98,7 +100,17 @@
end;
fun mode_indent x y = #indent (get_mode ()) x y;
-fun mode_markup x = #markup (get_mode ()) x;
+
+fun mode_markup m =
+ if m = Markup.none then ("", "")
+ else #markup (get_mode ()) m;
+
+fun add_markup m add =
+ let val (bg, en) = mode_markup m
+ in Buffer.add bg #> add #> Buffer.add en end;
+
+val output_spaces = Output.output o Symbol.spaces;
+val add_indent = Buffer.add o output_spaces;
@@ -109,13 +121,103 @@
String of string * int | (*text, length*)
Break of bool * int; (*mandatory flag, width if not taken*)
+fun length (Block (_, _, _, len)) = len
+ | length (String (_, len)) = len
+ | length (Break (_, wd)) = wd;
+
-(** output text **)
+(** derived operations to create formatting expressions **)
+
+val raw_str = String;
+val str = String o Output.output_width;
+
+fun brk wd = Break (false, wd);
+val fbrk = Break (true, 2);
+
+fun breaks prts = Library.separate (brk 1) prts;
+fun fbreaks prts = Library.separate fbrk prts;
+
+fun markup_block m (indent, es) =
+ let
+ fun sum [] k = k
+ | sum (e :: es) k = sum es (length e + k);
+ in Block (m, es, indent, sum es 0) end;
+
+val blk = markup_block Markup.none;
+fun block prts = blk (2, prts);
+val strs = block o breaks o map str;
+
+fun markup m prts = markup_block m (0, prts);
+fun keyword name = markup (Markup.keyword name) [str name];
+fun command name = markup (Markup.command name) [str name];
+
+fun markup_chunks m prts = markup m (fbreaks prts);
+val chunks = markup_chunks Markup.none;
+fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
+
+fun block_enclose (p1, p2) ps = chunks [(block o fbreaks) (p1 :: ps), p2];
+
+fun quote prt = blk (1, [str "\"", prt, str "\""]);
+fun backquote prt = blk (1, [str "`", prt, str "`"]);
+
+fun separate sep prts =
+ flat (Library.separate [str sep, brk 1] (map single prts));
+
+val commas = separate ",";
+
+fun enclose lpar rpar prts =
+ block (str lpar :: (prts @ [str rpar]));
+
+fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
-val output_spaces = Output.output o Symbol.spaces;
-val add_indent = Buffer.add o output_spaces;
-fun set_indent wd = Buffer.empty |> add_indent wd;
+val list = enum ",";
+fun str_list lpar rpar strs = list lpar rpar (map str strs);
+
+fun big_list name prts = block (fbreaks (str name :: prts));
+
+fun indent 0 prt = prt
+ | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
+
+fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
+ | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
+ | unbreakable (e as String _) = e;
+
+
+
+(** formatting **)
+
+(* margin *)
+
+fun make_margin_info m =
+ {margin = m, (*right margin, or page width*)
+ breakgain = m div 20, (*minimum added space required of a break*)
+ emergencypos = m div 2}; (*position too far to right*)
+
+val margin_info = ref (make_margin_info 76);
+fun setmargin m = margin_info := make_margin_info m;
+fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
+
+
+(* depth limitation *)
+
+val depth = ref 0; (*maximum depth; 0 means no limit*)
+fun setdepth dp = (depth := dp);
+
+local
+ fun pruning dp (Block (m, bes, indent, wd)) =
+ if dp > 0
+ then markup_block m (indent, map (pruning (dp - 1)) bes)
+ else str "..."
+ | pruning dp e = e
+in
+ fun prune e = if ! depth > 0 then pruning (! depth) e else e;
+end;
+
+
+(* formatted output *)
+
+local
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
@@ -153,24 +255,6 @@
nl = nl}
end;
-
-
-(** formatting **)
-
-(* margin *)
-
-fun make_margin_info m =
- {margin = m, (*right margin, or page width*)
- breakgain = m div 20, (*minimum added space required of a break*)
- emergencypos = m div 2}; (*position too far to right*)
-
-val margin_info = ref (make_margin_info 76);
-fun setmargin m = margin_info := make_margin_info m;
-fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
-
-
-(* format *)
-
(*Add the lengths of the expressions until the next Break; if no Break then
include "after", to account for text following this block.*)
fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
@@ -196,8 +280,8 @@
val pos'' = pos' mod emergencypos;
val block' =
if pos' < emergencypos then (ind |> add_indent indent, pos')
- else (set_indent pos'', pos'');
- val (bg, en) = if markup = Markup.none then ("", "") else mode_markup markup;
+ else (add_indent pos'' Buffer.empty, pos'');
+ val (bg, en) = mode_markup markup;
val btext: text = text
|> control bg
|> format (bes, block', breakdist (es, after))
@@ -217,107 +301,35 @@
else text |> newline |> indentation block)
end);
-
-(** Exported functions to create formatting expressions **)
-
-fun length (Block (_, _, _, len)) = len
- | length (String (_, len)) = len
- | length (Break(_, wd)) = wd;
-
-val raw_str = String;
-val str = String o Output.output_width;
+in
-fun brk wd = Break (false, wd);
-val fbrk = Break (true, 2);
+fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
-fun markup_block m (indent, es) =
- let
- fun sum [] k = k
- | sum (e :: es) k = sum es (length e + k);
- in Block (m, es, indent, sum es 0) end;
-
-val blk = markup_block Markup.none;
-
-fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
- | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
- | unbreakable (e as String _) = e;
+end;
-(* utils *)
-
-fun breaks prts = Library.separate (brk 1) prts;
-fun fbreaks prts = Library.separate fbrk prts;
-
-fun block prts = blk (2, prts);
-fun markup m prts = markup_block m (0, prts);
-
-fun keyword name = markup (Markup.keyword name) [str name];
-fun command name = markup (Markup.command name) [str name];
-
-val strs = block o breaks o map str;
-
-fun markup_chunks m prts = markup m (fbreaks prts);
-val chunks = markup_chunks Markup.none;
-
-fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
-fun block_enclose (p1, p2) ps = chunks [(block o fbreaks) (p1 :: ps), p2];
-
-fun quote prt = blk (1, [str "\"", prt, str "\""]);
-fun backquote prt = blk (1, [str "`", prt, str "`"]);
-
-fun separate sep prts =
- flat (Library.separate [str sep, brk 1] (map single prts));
-
-val commas = separate ",";
-
-fun enclose lpar rpar prts =
- block (str lpar :: (prts @ [str rpar]));
-
-fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
-
-val list = enum ",";
-fun str_list lpar rpar strs = list lpar rpar (map str strs);
+(* special output *)
-fun big_list name prts = block (fbreaks (str name :: prts));
-
-fun indent 0 prt = prt
- | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
-
-
-
-(** Pretty printing with depth limitation **)
-
-val depth = ref 0; (*maximum depth; 0 means no limit*)
-
-fun setdepth dp = (depth := dp);
+(*symbolic markup -- no formatting*)
+fun symbolic prt =
+ let
+ fun out (Block (m, prts, indent, _)) =
+ add_markup m (add_markup (Markup.block indent) (fold out prts))
+ | out (String (s, _)) = Buffer.add s
+ | out (Break (false, wd)) = add_markup (Markup.break wd) (Buffer.add (output_spaces wd))
+ | out (Break (true, _)) = add_markup Markup.fbreak I
+ in out prt Buffer.empty end;
-(*Recursively prune blocks, discarding all text exceeding depth dp*)
-fun pruning dp (Block (m, bes, indent, wd)) =
- if dp > 0
- then markup_block m (indent, map (pruning (dp - 1)) bes)
- else str "..."
- | pruning dp e = e;
-
-fun prune dp e = if dp > 0 then pruning dp e else e;
-
-fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);
-val output = Buffer.content o output_buffer;
-val string_of = Output.escape o output;
-val writeln = Output.writeln o string_of;
-
-
-(*Create a single flat string: no line breaking*)
-fun str_of prt =
+(*unformatted output*)
+fun unformatted prt =
let
- fun fmt (Block (m, prts, _, _)) =
- let val (bg, en) = mode_markup m
- in Buffer.add bg #> fold fmt prts #> Buffer.add en end
+ fun fmt (Block (m, prts, _, _)) = add_markup m (fold fmt prts)
| fmt (String (s, _)) = Buffer.add s
| fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
| fmt (Break (true, _)) = Buffer.add (output_spaces 1);
- in Output.escape (Buffer.content (fmt (prune (! depth) prt) Buffer.empty)) end;
+ in fmt (prune prt) Buffer.empty end;
-(*part of the interface to the ML toplevel pretty printers*)
+(*ML toplevel pretty printing*)
fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
let
fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
@@ -326,7 +338,21 @@
| pp (Break (true, _)) = put_fbrk ()
and pp_lst [] = ()
| pp_lst (prt :: prts) = (pp prt; pp_lst prts);
- in pp (prune (! depth) prt) end;
+ in pp (prune prt) end;
+
+
+(* output interfaces *)
+
+val symbolicN = "pretty_symbolic";
+
+fun output_buffer prt =
+ if print_mode_active symbolicN then symbolic prt
+ else formatted prt;
+
+val output = Buffer.content o output_buffer;
+val string_of = Output.escape o output;
+val str_of = Output.escape o Buffer.content o unformatted;
+val writeln = Output.writeln o string_of;