src/Pure/Syntax/pretty.ML
changeset 6116 8ba2f25610f7
parent 6115 c70bce7deb0f
child 6117 f9aad8ccd590
     1.1 --- a/src/Pure/Syntax/pretty.ML	Wed Jan 13 12:16:34 1999 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,249 +0,0 @@
     1.4 -(*  Title:      Pure/Syntax/pretty.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Generic pretty printing module.
    1.10 -
    1.11 -Loosely based on
    1.12 -  D. C. Oppen, "Pretty Printing",
    1.13 -  ACM Transactions on Programming Languages and Systems (1980), 465-483.
    1.14 -
    1.15 -The object to be printed is given as a tree with indentation and line
    1.16 -breaking information.  A "break" inserts a newline if the text until
    1.17 -the next break is too long to fit on the current line.  After the newline,
    1.18 -text is indented to the level of the enclosing block.  Normally, if a block
    1.19 -is broken then all enclosing blocks will also be broken.  Only "inconsistent
    1.20 -breaks" are provided.
    1.21 -
    1.22 -The stored length of a block is used in breakdist (to treat each inner block as
    1.23 -a unit for breaking).
    1.24 -*)
    1.25 -
    1.26 -type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
    1.27 -  (unit -> unit) * (unit -> unit);
    1.28 -
    1.29 -signature PRETTY =
    1.30 -  sig
    1.31 -  type T
    1.32 -  val str: string -> T
    1.33 -  val strlen: string -> int -> T
    1.34 -  val sym: string -> T
    1.35 -  val spc: int -> T
    1.36 -  val brk: int -> T
    1.37 -  val fbrk: T
    1.38 -  val blk: int * T list -> T
    1.39 -  val lst: string * string -> T list -> T
    1.40 -  val quote: T -> T
    1.41 -  val commas: T list -> T list
    1.42 -  val breaks: T list -> T list
    1.43 -  val fbreaks: T list -> T list
    1.44 -  val block: T list -> T
    1.45 -  val strs: string list -> T
    1.46 -  val enclose: string -> string -> T list -> T
    1.47 -  val list: string -> string -> T list -> T
    1.48 -  val str_list: string -> string -> string list -> T
    1.49 -  val big_list: string -> T list -> T
    1.50 -  val string_of: T -> string
    1.51 -  val writeln: T -> unit
    1.52 -  val str_of: T -> string
    1.53 -  val pprint: T -> pprint_args -> unit
    1.54 -  val setdepth: int -> unit
    1.55 -  val setmargin: int -> unit
    1.56 -  end;
    1.57 -
    1.58 -structure Pretty : PRETTY =
    1.59 -struct
    1.60 -
    1.61 -(*printing items: compound phrases, strings, and breaks*)
    1.62 -datatype T =
    1.63 -  Block of T list * int * int |         (*body, indentation, length*)
    1.64 -  String of string * int |              (*text, length*)
    1.65 -  Break of bool * int;                  (*mandatory flag, width if not taken*);
    1.66 -
    1.67 -(*Add the lengths of the expressions until the next Break; if no Break then
    1.68 -  include "after", to account for text following this block. *)
    1.69 -fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
    1.70 -  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
    1.71 -  | breakdist (Break _ :: es, after) = 0
    1.72 -  | breakdist ([], after) = after;
    1.73 -
    1.74 -fun repstring a 0 = ""
    1.75 -  | repstring a 1 = a
    1.76 -  | repstring a k =
    1.77 -      if k mod 2 = 0 then repstring(a^a) (k div 2)
    1.78 -                     else repstring(a^a) (k div 2) ^ a;
    1.79 -
    1.80 -(*** Type for lines of text: string, # of lines, position on line ***)
    1.81 -
    1.82 -type text = {tx: string, nl: int, pos: int};
    1.83 -
    1.84 -val emptytext = {tx="", nl=0, pos=0};
    1.85 -
    1.86 -fun blanks wd {tx,nl,pos} =
    1.87 -    {tx  = tx ^ repstring " " wd,
    1.88 -     nl  = nl,
    1.89 -     pos = pos+wd};
    1.90 -
    1.91 -fun newline {tx,nl,pos} =
    1.92 -    {tx  = tx ^ "\n",
    1.93 -     nl  = nl+1,
    1.94 -     pos = 0};
    1.95 -
    1.96 -fun string s len {tx,nl,pos:int} =
    1.97 -    {tx  = tx ^ s,
    1.98 -     nl  = nl,
    1.99 -     pos = pos + len};
   1.100 -
   1.101 -
   1.102 -(*** Formatting ***)
   1.103 -
   1.104 -(* margin *)
   1.105 -
   1.106 -(*example values*)
   1.107 -val margin      = ref 80        (*right margin, or page width*)
   1.108 -and breakgain   = ref 4         (*minimum added space required of a break*)
   1.109 -and emergencypos = ref 40;      (*position too far to right*)
   1.110 -
   1.111 -fun setmargin m =
   1.112 -    (margin     := m;
   1.113 -     breakgain  := !margin div 20;
   1.114 -     emergencypos := !margin div 2);
   1.115 -
   1.116 -val () = setmargin 76;
   1.117 -
   1.118 -
   1.119 -(*Search for the next break (at this or higher levels) and force it to occur*)
   1.120 -fun forcenext [] = []
   1.121 -  | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   1.122 -  | forcenext (e :: es) = e :: forcenext es;
   1.123 -
   1.124 -(*es is list of expressions to print;
   1.125 -  blockin is the indentation of the current block;
   1.126 -  after is the width of the following context until next break. *)
   1.127 -fun format ([], _, _) text = text
   1.128 -  | format (e::es, blockin, after) (text as {pos,nl,...}) =
   1.129 -    (case e of
   1.130 -       Block(bes,indent,wd) =>
   1.131 -         let val blockin' = (pos + indent) mod !emergencypos
   1.132 -             val btext = format(bes, blockin', breakdist(es,after)) text
   1.133 -             (*If this block was broken then force the next break.*)
   1.134 -             val es2 = if nl < #nl(btext) then forcenext es else es
   1.135 -         in  format (es2,blockin,after) btext  end
   1.136 -     | String (s, len) => format (es,blockin,after) (string s len text)
   1.137 -     | Break(force,wd) => (*no break if text to next break fits on this line
   1.138 -                            or if breaking would add only breakgain to space *)
   1.139 -           format (es,blockin,after)
   1.140 -               (if not force andalso
   1.141 -                   pos+wd <= Int.max(!margin - breakdist(es,after),
   1.142 -                                     blockin + !breakgain)
   1.143 -                then blanks wd text  (*just insert wd blanks*)
   1.144 -                else blanks blockin (newline text)));
   1.145 -
   1.146 -
   1.147 -(*** Exported functions to create formatting expressions ***)
   1.148 -
   1.149 -fun length (Block (_, _, len)) = len
   1.150 -  | length (String (_, len)) = len
   1.151 -  | length (Break(_, wd)) = wd;
   1.152 -
   1.153 -fun str s = String (s, size s);
   1.154 -fun strlen s len = String (s, len);
   1.155 -fun sym s = String (s, Symbol.size s);
   1.156 -
   1.157 -fun spc n = str (repstring " " n);
   1.158 -
   1.159 -fun brk wd = Break (false, wd);
   1.160 -val fbrk = Break (true, 0);
   1.161 -
   1.162 -fun blk (indent, es) =
   1.163 -  let
   1.164 -    fun sum([], k) = k
   1.165 -      | sum(e :: es, k) = sum (es, length e + k);
   1.166 -  in Block (es, indent, sum (es, 0)) end;
   1.167 -
   1.168 -(*Join the elements of es as a comma-separated list, bracketted by lp and rp*)
   1.169 -fun lst(lp,rp) es =
   1.170 -  let fun add(e,es) = str"," :: brk 1 :: e :: es;
   1.171 -      fun list(e :: (es as _::_)) = str lp :: e :: foldr add (es,[str rp])
   1.172 -        | list(e::[]) = [str lp, e, str rp]
   1.173 -        | list([]) = []
   1.174 -  in blk(size lp, list es) end;
   1.175 -
   1.176 -
   1.177 -(* utils *)
   1.178 -
   1.179 -fun quote prt =
   1.180 -  blk (1, [str "\"", prt, str "\""]);
   1.181 -
   1.182 -fun commas prts =
   1.183 -  flat (separate [str ",", brk 1] (map (fn x => [x]) prts));
   1.184 -
   1.185 -fun breaks prts = separate (brk 1) prts;
   1.186 -
   1.187 -fun fbreaks prts = separate fbrk prts;
   1.188 -
   1.189 -fun block prts = blk (2, prts);
   1.190 -
   1.191 -val strs = block o breaks o (map str);
   1.192 -
   1.193 -fun enclose lpar rpar prts =
   1.194 -  block (str lpar :: (prts @ [str rpar]));
   1.195 -
   1.196 -fun list lpar rpar prts =
   1.197 -  enclose lpar rpar (commas prts);
   1.198 -
   1.199 -fun str_list lpar rpar strs =
   1.200 -  list lpar rpar (map str strs);
   1.201 -
   1.202 -fun big_list name prts =
   1.203 -  block (fbreaks (str name :: prts));
   1.204 -
   1.205 -
   1.206 -
   1.207 -(*** Pretty printing with depth limitation ***)
   1.208 -
   1.209 -val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   1.210 -
   1.211 -fun setdepth dp = (depth := dp);
   1.212 -
   1.213 -(*Recursively prune blocks, discarding all text exceeding depth dp*)
   1.214 -fun pruning dp (Block(bes,indent,wd)) =
   1.215 -      if dp>0 then blk(indent, map (pruning(dp-1)) bes)
   1.216 -              else str "..."
   1.217 -  | pruning dp e = e;
   1.218 -
   1.219 -fun prune dp e = if dp>0 then pruning dp e else e;
   1.220 -
   1.221 -
   1.222 -fun string_of e = #tx (format ([prune (!depth) e], 0, 0) emptytext);
   1.223 -
   1.224 -val writeln = writeln o string_of;
   1.225 -
   1.226 -
   1.227 -(*Create a single flat string: no line breaking*)
   1.228 -fun str_of prt =
   1.229 -  let
   1.230 -    fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   1.231 -      | s_of (String (s, _)) = s
   1.232 -      | s_of (Break (false, wd)) = repstring " " wd
   1.233 -      | s_of (Break (true, _)) = " ";
   1.234 -  in
   1.235 -    s_of (prune (! depth) prt)
   1.236 -  end;
   1.237 -
   1.238 -(*Part of the interface to the Poly/ML and New Jersey ML pretty printers*)
   1.239 -fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   1.240 -  let
   1.241 -    fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
   1.242 -      | pp (String (s, _)) = put_str s
   1.243 -      | pp (Break (false, wd)) = put_brk wd
   1.244 -      | pp (Break (true, _)) = put_fbrk ()
   1.245 -    and pp_lst [] = ()
   1.246 -      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
   1.247 -  in
   1.248 -    pp (prune (! depth) prt)
   1.249 -  end;
   1.250 -
   1.251 -
   1.252 -end;