src/Pure/General/pretty.ML
changeset 10952 b520e4f1313b
parent 9730 11d137b25555
child 12421 54c06c1f88b8
     1.1 --- a/src/Pure/General/pretty.ML	Sun Jan 21 19:52:32 2001 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sun Jan 21 19:53:29 2001 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/General/pretty.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Author:	Markus Wenzel, TU Munich
     1.8 +    Author:     Markus Wenzel, TU Munich
     1.9      License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11  Generic pretty printing module.
    1.12 @@ -56,51 +56,53 @@
    1.13  structure Pretty : PRETTY =
    1.14  struct
    1.15  
    1.16 -(*printing items: compound phrases, strings, and breaks*)
    1.17 +
    1.18 +(** printing items: compound phrases, strings, and breaks **)
    1.19 +
    1.20  datatype T =
    1.21    Block of T list * int * int |         (*body, indentation, length*)
    1.22    String of string * int |              (*text, length*)
    1.23    Break of bool * int;                  (*mandatory flag, width if not taken*);
    1.24  
    1.25 -(*Add the lengths of the expressions until the next Break; if no Break then
    1.26 -  include "after", to account for text following this block. *)
    1.27 -fun breakdist (Block(_,_,len)::es, after) = len + breakdist(es, after)
    1.28 -  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
    1.29 -  | breakdist (Break _ :: es, after) = 0
    1.30 -  | breakdist ([], after) = after;
    1.31 -
    1.32 -fun repstring a 0 = ""
    1.33 -  | repstring a 1 = a
    1.34 -  | repstring a k =
    1.35 -      if k mod 2 = 0 then repstring(a^a) (k div 2)
    1.36 -      else repstring(a^a) (k div 2) ^ a;
    1.37 -
    1.38 -val spaces = repstring " ";
    1.39  
    1.40  
    1.41 -(*** Type for lines of text: string, # of lines, position on line ***)
    1.42 +(** output text **)
    1.43 +
    1.44 +val output_spaces = Symbol.output o Symbol.spaces;
    1.45 +val add_indent = Buffer.add o output_spaces;
    1.46 +fun set_indent wd = Buffer.empty |> add_indent wd;
    1.47  
    1.48 -type text = {tx: Buffer.T, nl: int, pos: int};
    1.49 -
    1.50 -val emptytext = {tx = Buffer.empty, nl = 0, pos = 0};
    1.51 +val empty =
    1.52 + {tx = Buffer.empty,
    1.53 +  ind = Buffer.empty,
    1.54 +  pos = 0,
    1.55 +  nl = 0};
    1.56  
    1.57 -fun blanks wd {tx, nl, pos} =
    1.58 -    {tx  = Buffer.add (Symbol.output (spaces wd)) tx,
    1.59 -     nl  = nl,
    1.60 -     pos = pos+wd};
    1.61 +fun newline {tx, ind, pos, nl} =
    1.62 + {tx = Buffer.add (Symbol.output "\n") tx,
    1.63 +  ind = Buffer.empty,
    1.64 +  pos = 0,
    1.65 +  nl = nl + 1};
    1.66  
    1.67 -fun newline {tx, nl, pos} =
    1.68 -    {tx  = Buffer.add (Symbol.output "\n") tx,
    1.69 -     nl  = nl + 1,
    1.70 -     pos = 0};
    1.71 +fun string (s, len) {tx, ind, pos: int, nl} =
    1.72 + {tx = Buffer.add s tx,
    1.73 +  ind = Buffer.add s ind,
    1.74 +  pos = pos + len,
    1.75 +  nl = nl};
    1.76 +
    1.77 +fun blanks wd = string (output_spaces wd, wd);
    1.78  
    1.79 -fun string s len {tx, nl, pos:int} =
    1.80 -    {tx  = Buffer.add s tx,
    1.81 -     nl  = nl,
    1.82 -     pos = pos + len};
    1.83 +fun indentation (buf, len) {tx, ind, pos, nl} =
    1.84 +  let val s = Buffer.content buf in
    1.85 +   {tx = Buffer.add (Symbol.indent (s, len)) tx,
    1.86 +    ind = Buffer.add s ind,
    1.87 +    pos = pos + len,
    1.88 +    nl = nl}
    1.89 +  end;
    1.90  
    1.91  
    1.92 -(*** Formatting ***)
    1.93 +
    1.94 +(** formatting **)
    1.95  
    1.96  (* margin *)
    1.97  
    1.98 @@ -113,32 +115,50 @@
    1.99  fun setmargin m = margin_info := make_margin_info m;
   1.100  fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
   1.101  
   1.102 -(*Search for the next break (at this or higher levels) and force it to occur*)
   1.103 +
   1.104 +(* format *)
   1.105 +
   1.106 +(*Add the lengths of the expressions until the next Break; if no Break then
   1.107 +  include "after", to account for text following this block.*)
   1.108 +fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after)
   1.109 +  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
   1.110 +  | breakdist (Break _ :: es, after) = 0
   1.111 +  | breakdist ([], after) = after;
   1.112 +
   1.113 +(*Search for the next break (at this or higher levels) and force it to occur.*)
   1.114  fun forcenext [] = []
   1.115 -  | forcenext (Break(_,wd) :: es) = Break(true,0) :: es
   1.116 +  | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
   1.117    | forcenext (e :: es) = e :: forcenext es;
   1.118  
   1.119  (*es is list of expressions to print;
   1.120    blockin is the indentation of the current block;
   1.121 -  after is the width of the following context until next break. *)
   1.122 +  after is the width of the following context until next break.*)
   1.123  fun format ([], _, _) text = text
   1.124 -  | format (e::es, blockin, after) (text as {pos,nl,...}) =
   1.125 -    (case e of
   1.126 -       Block(bes,indent,wd) =>
   1.127 -         let val blockin' = (pos + indent) mod #emergencypos (! margin_info)
   1.128 -             val btext = format(bes, blockin', breakdist(es,after)) text
   1.129 -             (*If this block was broken then force the next break.*)
   1.130 -             val es2 = if nl < #nl(btext) then forcenext es else es
   1.131 -         in  format (es2,blockin,after) btext  end
   1.132 -     | String (s, len) => format (es,blockin,after) (string s len text)
   1.133 -     | Break(force,wd) => (*no break if text to next break fits on this line
   1.134 -                            or if breaking would add only breakgain to space *)
   1.135 -           format (es,blockin,after)
   1.136 -               (if not force andalso
   1.137 -                   pos+wd <= Int.max(#margin (! margin_info) - breakdist(es,after),
   1.138 -                                     blockin + #breakgain (! margin_info))
   1.139 -                then blanks wd text  (*just insert wd blanks*)
   1.140 -                else blanks blockin (newline text)));
   1.141 +  | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
   1.142 +      (case e of
   1.143 +        Block (bes, indent, wd) =>
   1.144 +          let
   1.145 +            val {emergencypos, ...} = ! margin_info;
   1.146 +            val pos' = pos + indent;
   1.147 +            val pos'' = pos' mod emergencypos;
   1.148 +            val block' =
   1.149 +              if pos' < emergencypos then (ind |> add_indent indent, pos')
   1.150 +              else (set_indent pos'', pos'');
   1.151 +            val btext = format (bes, block', breakdist (es, after)) text;
   1.152 +            (*if this block was broken then force the next break*)
   1.153 +            val es2 = if nl < #nl btext then forcenext es else es;
   1.154 +          in format (es2, block, after) btext end
   1.155 +      | String str => format (es, block, after) (string str text)
   1.156 +      | Break (force, wd) =>
   1.157 +          let val {margin, breakgain, ...} = ! margin_info in
   1.158 +            (*no break if text to next break fits on this line
   1.159 +              or if breaking would add only breakgain to space*)
   1.160 +            format (es, block, after)
   1.161 +              (if not force andalso
   1.162 +                  pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   1.163 +                then text |> blanks wd  (*just insert wd blanks*)
   1.164 +                else text |> newline |> indentation block)
   1.165 +          end);
   1.166  
   1.167  
   1.168  (*** Exported functions to create formatting expressions ***)
   1.169 @@ -184,7 +204,7 @@
   1.170  fun chunks prts = blk (0, fbreaks prts);
   1.171  
   1.172  fun indent 0 prt = prt
   1.173 -  | indent n prt = blk (0, [str (spaces n), prt]);
   1.174 +  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
   1.175  
   1.176  
   1.177  (*** Pretty printing with depth limitation ***)
   1.178 @@ -199,11 +219,9 @@
   1.179                else str "..."
   1.180    | pruning dp e = e;
   1.181  
   1.182 -fun prune dp e = if dp>0 then pruning dp e else e;
   1.183 -
   1.184 +fun prune dp e = if dp > 0 then pruning dp e else e;
   1.185  
   1.186 -fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], 0, 0) emptytext));
   1.187 -
   1.188 +fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
   1.189  val writeln = writeln o string_of;
   1.190  
   1.191  
   1.192 @@ -212,8 +230,8 @@
   1.193    let
   1.194      fun s_of (Block (prts, _, _)) = implode (map s_of prts)
   1.195        | s_of (String (s, _)) = s
   1.196 -      | s_of (Break (false, wd)) = Symbol.output (spaces wd)
   1.197 -      | s_of (Break (true, _)) = Symbol.output " ";
   1.198 +      | s_of (Break (false, wd)) = output_spaces wd
   1.199 +      | s_of (Break (true, _)) = output_spaces 1;
   1.200    in s_of (prune (! depth) prt) end;
   1.201  
   1.202  (*part of the interface to the ML toplevel pretty printers*)