--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/pretty.ML Wed Jan 13 12:44:33 1999 +0100
@@ -0,0 +1,249 @@
+(* Title: Pure/Syntax/pretty.ML
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1991 University of Cambridge
+
+Generic pretty printing module.
+
+Loosely based on
+ D. C. Oppen, "Pretty Printing",
+ ACM Transactions on Programming Languages and Systems (1980), 465-483.
+
+The object to be printed is given as a tree with indentation and line
+breaking information. A "break" inserts a newline if the text until
+the next break is too long to fit on the current line. After the newline,
+text is indented to the level of the enclosing block. Normally, if a block
+is broken then all enclosing blocks will also be broken. Only "inconsistent
+breaks" are provided.
+
+The stored length of a block is used in breakdist (to treat each inner block as
+a unit for breaking).
+*)
+
+type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
+ (unit -> unit) * (unit -> unit);
+
+signature PRETTY =
+ sig
+ type T
+ val str: string -> T
+ val strlen: string -> int -> T
+ val sym: string -> T
+ val spc: int -> T
+ val brk: int -> T
+ val fbrk: T
+ val blk: int * T list -> T
+ val lst: string * string -> T list -> T
+ val quote: T -> T
+ val commas: T list -> T list
+ val breaks: T list -> T list
+ val fbreaks: T list -> T list
+ val block: T list -> T
+ val strs: string list -> T
+ val enclose: string -> string -> T list -> T
+ val list: string -> string -> T list -> T
+ val str_list: string -> string -> string list -> T
+ val big_list: string -> T list -> T
+ val string_of: T -> string
+ val writeln: T -> unit
+ val str_of: T -> string
+ val pprint: T -> pprint_args -> unit
+ val setdepth: int -> unit
+ val setmargin: int -> unit
+ end;
+
+structure Pretty : PRETTY =
+struct
+
+(*printing items: compound phrases, strings, and breaks*)
+datatype T =
+ Block of T list * int * int | (*body, indentation, length*)
+ String of string * int | (*text, length*)
+ Break of bool * int; (*mandatory flag, width if not taken*);
+
+(*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)
+ | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
+ | breakdist (Break _ :: es, after) = 0
+ | breakdist ([], after) = after;
+
+fun repstring a 0 = ""
+ | repstring a 1 = a
+ | repstring a k =
+ if k mod 2 = 0 then repstring(a^a) (k div 2)
+ else repstring(a^a) (k div 2) ^ a;
+
+(*** Type for lines of text: string, # of lines, position on line ***)
+
+type text = {tx: string, nl: int, pos: int};
+
+val emptytext = {tx="", nl=0, pos=0};
+
+fun blanks wd {tx,nl,pos} =
+ {tx = tx ^ repstring " " wd,
+ nl = nl,
+ pos = pos+wd};
+
+fun newline {tx,nl,pos} =
+ {tx = tx ^ "\n",
+ nl = nl+1,
+ pos = 0};
+
+fun string s len {tx,nl,pos:int} =
+ {tx = tx ^ s,
+ nl = nl,
+ pos = pos + len};
+
+
+(*** Formatting ***)
+
+(* margin *)
+
+(*example values*)
+val margin = ref 80 (*right margin, or page width*)
+and breakgain = ref 4 (*minimum added space required of a break*)
+and emergencypos = ref 40; (*position too far to right*)
+
+fun setmargin m =
+ (margin := m;
+ breakgain := !margin div 20;
+ emergencypos := !margin div 2);
+
+val () = setmargin 76;
+
+
+(*Search for the next break (at this or higher levels) and force it to occur*)
+fun forcenext [] = []
+ | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
+ | forcenext (e :: es) = e :: forcenext es;
+
+(*es is list of expressions to print;
+ blockin is the indentation of the current block;
+ after is the width of the following context until next break. *)
+fun format ([], _, _) text = text
+ | format (e::es, blockin, after) (text as {pos,nl,...}) =
+ (case e of
+ Block(bes,indent,wd) =>
+ let val blockin' = (pos + indent) mod !emergencypos
+ val btext = format(bes, blockin', breakdist(es,after)) text
+ (*If this block was broken then force the next break.*)
+ val es2 = if nl < #nl(btext) then forcenext es else es
+ in format (es2,blockin,after) btext end
+ | String (s, len) => format (es,blockin,after) (string s len text)
+ | Break(force,wd) => (*no break if text to next break fits on this line
+ or if breaking would add only breakgain to space *)
+ format (es,blockin,after)
+ (if not force andalso
+ pos+wd <= Int.max(!margin - breakdist(es,after),
+ blockin + !breakgain)
+ then blanks wd text (*just insert wd blanks*)
+ else blanks blockin (newline text)));
+
+
+(*** Exported functions to create formatting expressions ***)
+
+fun length (Block (_, _, len)) = len
+ | length (String (_, len)) = len
+ | length (Break(_, wd)) = wd;
+
+fun str s = String (s, size s);
+fun strlen s len = String (s, len);
+fun sym s = String (s, Symbol.size s);
+
+fun spc n = str (repstring " " n);
+
+fun brk wd = Break (false, wd);
+val fbrk = Break (true, 0);
+
+fun blk (indent, es) =
+ let
+ fun sum([], k) = k
+ | sum(e :: es, k) = sum (es, length e + k);
+ in Block (es, indent, sum (es, 0)) end;
+
+(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
+fun lst(lp,rp) es =
+ let fun add(e,es) = str"," :: brk 1 :: e :: es;
+ fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
+ | list(e::[]) = [str lp, e, str rp]
+ | list([]) = []
+ in blk(size lp, list es) end;
+
+
+(* utils *)
+
+fun quote prt =
+ blk (1, [str "\"", prt, str "\""]);
+
+fun commas prts =
+ flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
+
+fun breaks prts = separate (brk 1) prts;
+
+fun fbreaks prts = separate fbrk prts;
+
+fun block prts = blk (2, prts);
+
+val strs = block o breaks o (map str);
+
+fun enclose lpar rpar prts =
+ block (str lpar :: (prts @ [str rpar]));
+
+fun list lpar rpar prts =
+ enclose lpar rpar (commas prts);
+
+fun str_list lpar rpar strs =
+ list lpar rpar (map str strs);
+
+fun big_list name prts =
+ block (fbreaks (str name :: prts));
+
+
+
+(*** Pretty printing with depth limitation ***)
+
+val depth = ref 0; (*maximum depth; 0 means no limit*)
+
+fun setdepth dp = (depth := dp);
+
+(*Recursively prune blocks, discarding all text exceeding depth dp*)
+fun pruning dp (Block(bes,indent,wd)) =
+ if dp>0 then blk(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 string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
+
+val writeln = writeln o string_of;
+
+
+(*Create a single flat string: no line breaking*)
+fun str_of prt =
+ let
+ fun s_of (Block (prts, _, _)) = implode (map s_of prts)
+ | s_of (String (s, _)) = s
+ | s_of (Break (false, wd)) = repstring " " wd
+ | s_of (Break (true, _)) = " ";
+ in
+ s_of (prune (! depth) prt)
+ end;
+
+(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
+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 ())
+ | pp (String (s, _)) = put_str s
+ | pp (Break (false, wd)) = put_brk wd
+ | pp (Break (true, _)) = put_fbrk ()
+ and pp_lst [] = ()
+ | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
+ in
+ pp (prune (! depth) prt)
+ end;
+
+
+end;