--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/pretty.ML Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,191 @@
+(* Title: Pure/Syntax/pretty
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1991 University of Cambridge
+
+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).
+*)
+
+(* FIXME improve? *)
+type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) * (unit -> unit);
+
+signature PRETTY =
+ sig
+ type T
+ val blk : int * T list -> T
+ val brk : int -> T
+ val fbrk : T
+ val str : string -> T
+ val lst : string * string -> T list -> T
+ val quote : T -> T
+ val string_of : T -> string
+ val str_of : T -> string
+ val pprint : T -> pprint_args -> unit
+ val setdepth: int -> unit
+ val setmargin: int -> unit
+ end;
+
+functor PrettyFun () : PRETTY =
+struct
+
+(*Printing items: compound phrases, strings, and breaks*)
+datatype T = Block of T list * int * int (*indentation, length*)
+ | String of string
+ | 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 :: es, after) = size s + 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 {tx,nl,pos} =
+ {tx = tx ^ s,
+ nl = nl,
+ pos = pos + size(s)};
+
+(*** Formatting ***)
+
+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);
+
+fun forcenext [] = []
+ | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
+ | forcenext (e :: es) = e :: forcenext es;
+
+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
+ val es2 = if nl < #nl(btext) then forcenext es
+ else es
+ in format (es2,blockin,after) btext end
+ | String s => format (es,blockin,after) (string s text)
+ | Break(force,wd) => (* no break if text fits on this line
+ or if breaking would add only breakgain to space *)
+ format (es,blockin,after)
+ (if not force andalso
+ pos+wd <= max[!margin - breakdist(es,after),
+ blockin + !breakgain]
+ then blanks wd text
+ else blanks blockin (newline text)));
+
+(*** Exported functions to create formatting expressions ***)
+
+fun length (Block(_,_,len)) = len
+ | length (String s) = size s
+ | length (Break(_,wd)) = wd;
+
+val str = String
+and fbrk = Break(true,0);
+
+fun brk wd = Break(false,wd);
+
+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;
+
+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;
+
+fun quote prt = blk (1, [str "\"", prt, str "\""]);
+
+
+(*** Pretty printing with depth limitation ***)
+
+val depth = ref 0; (*maximum depth; 0 means no limit*)
+
+fun setdepth dp = (depth := dp);
+
+
+fun pruning dp (Block(bes,indent,wd)) =
+ if dp>0 then blk(indent, map (pruning(dp-1)) bes)
+ else String"..."
+ | 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);
+
+
+fun brk_width (force, wd) = if force andalso wd = 0 then 1 else wd;
+
+fun str_of prt =
+ let
+ fun s_of (Block (prts, _, _)) = implode (map s_of prts)
+ | s_of (String s) = s
+ | s_of (Break f_w) = repstring " " (brk_width f_w);
+ in
+ s_of (prune (! depth) prt)
+ end;
+
+
+fun pprint prt (put_str, begin_blk, put_brk, end_blk) =
+ let
+ fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
+ | pp (String s) = put_str s
+ | pp (Break f_w) = put_brk (brk_width f_w)
+ and pp_lst [] = ()
+ | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
+ in
+ pp (prune (! depth) prt)
+ end;
+
+
+(*** Initialization ***)
+
+val () = setmargin 80;
+
+end;
+