src/Pure/General/pretty.ML
author wenzelm
Thu Dec 17 17:32:01 2015 +0100 (2015-12-17)
changeset 61862 e2a9e46ac0fb
parent 56334 6b3739fee456
child 61863 931792ce2d83
permissions -rw-r--r--
support pretty break indent, like underlying ML systems;
     1 (*  Title:      Pure/General/pretty.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Markus Wenzel, TU Munich
     4 
     5 Generic pretty printing module.
     6 
     7 Loosely based on
     8   D. C. Oppen, "Pretty Printing",
     9   ACM Transactions on Programming Languages and Systems (1980), 465-483.
    10 
    11 The object to be printed is given as a tree with indentation and line
    12 breaking information.  A "break" inserts a newline if the text until
    13 the next break is too long to fit on the current line.  After the newline,
    14 text is indented to the level of the enclosing block.  Normally, if a block
    15 is broken then all enclosing blocks will also be broken.  Only "inconsistent
    16 breaks" are provided.
    17 
    18 The stored length of a block is used in breakdist (to treat each inner block as
    19 a unit for breaking).
    20 *)
    21 
    22 signature PRETTY =
    23 sig
    24   val spaces: int -> string
    25   val default_indent: string -> int -> Output.output
    26   val add_mode: string -> (string -> int -> Output.output) -> unit
    27   type T
    28   val str: string -> T
    29   val brk: int -> T
    30   val brk_indent: int -> int -> T
    31   val fbrk: T
    32   val breaks: T list -> T list
    33   val fbreaks: T list -> T list
    34   val blk: int * T list -> T
    35   val block: T list -> T
    36   val strs: string list -> T
    37   val raw_markup: Output.output * Output.output -> int * T list -> T
    38   val markup: Markup.T -> T list -> T
    39   val mark: Markup.T -> T -> T
    40   val mark_str: Markup.T * string -> T
    41   val marks_str: Markup.T list * string -> T
    42   val item: T list -> T
    43   val text_fold: T list -> T
    44   val keyword1: string -> T
    45   val keyword2: string -> T
    46   val text: string -> T list
    47   val paragraph: T list -> T
    48   val para: string -> T
    49   val quote: T -> T
    50   val backquote: T -> T
    51   val cartouche: T -> T
    52   val separate: string -> T list -> T list
    53   val commas: T list -> T list
    54   val enclose: string -> string -> T list -> T
    55   val enum: string -> string -> string -> T list -> T
    56   val position: Position.T -> T
    57   val list: string -> string -> T list -> T
    58   val str_list: string -> string -> string list -> T
    59   val big_list: string -> T list -> T
    60   val indent: int -> T -> T
    61   val unbreakable: T -> T
    62   val margin_default: int Unsynchronized.ref
    63   val symbolicN: string
    64   val output_buffer: int option -> T -> Buffer.T
    65   val output: int option -> T -> Output.output
    66   val string_of_margin: int -> T -> string
    67   val string_of: T -> string
    68   val writeln: T -> unit
    69   val symbolic_output: T -> Output.output
    70   val symbolic_string_of: T -> string
    71   val str_of: T -> string
    72   val markup_chunks: Markup.T -> T list -> T
    73   val chunks: T list -> T
    74   val chunks2: T list -> T
    75   val block_enclose: T * T -> T list -> T
    76   val writeln_chunks: T list -> unit
    77   val writeln_chunks2: T list -> unit
    78   val to_ML: T -> ML_Pretty.pretty
    79   val from_ML: ML_Pretty.pretty -> T
    80 end;
    81 
    82 structure Pretty: PRETTY =
    83 struct
    84 
    85 (** spaces **)
    86 
    87 local
    88   val small_spaces = Vector.tabulate (65, fn i => replicate_string i Symbol.space);
    89 in
    90   fun spaces k =
    91     if k < 64 then Vector.sub (small_spaces, k)
    92     else
    93       replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
    94         Vector.sub (small_spaces, k mod 64);
    95 end;
    96 
    97 
    98 
    99 (** print mode operations **)
   100 
   101 fun default_indent (_: string) = spaces;
   102 
   103 local
   104   val default = {indent = default_indent};
   105   val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
   106 in
   107   fun add_mode name indent =
   108     Synchronized.change modes (fn tab =>
   109       (if not (Symtab.defined tab name) then ()
   110        else warning ("Redefining pretty mode " ^ quote name);
   111        Symtab.update (name, {indent = indent}) tab));
   112   fun get_mode () =
   113     the_default default
   114       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
   115 end;
   116 
   117 fun mode_indent x y = #indent (get_mode ()) x y;
   118 
   119 val output_spaces = Output.output o spaces;
   120 val add_indent = Buffer.add o output_spaces;
   121 
   122 
   123 
   124 (** printing items: compound phrases, strings, and breaks **)
   125 
   126 abstype T =
   127     Block of (Output.output * Output.output) * T list * int * int
   128       (*markup output, body, indentation, length*)
   129   | String of Output.output * int  (*text, length*)
   130   | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
   131 with
   132 
   133 fun length (Block (_, _, _, len)) = len
   134   | length (String (_, len)) = len
   135   | length (Break (_, wd, _)) = wd;
   136 
   137 
   138 
   139 (** derived operations to create formatting expressions **)
   140 
   141 val str = String o Output.output_width;
   142 
   143 fun brk wd = Break (false, wd, 0);
   144 fun brk_indent wd ind = Break (false, wd, ind);
   145 val fbrk = Break (true, 1, 0);
   146 
   147 fun breaks prts = Library.separate (brk 1) prts;
   148 fun fbreaks prts = Library.separate fbrk prts;
   149 
   150 fun raw_markup m (indent, es) =
   151   let
   152     fun sum [] k = k
   153       | sum (e :: es) k = sum es (length e + k);
   154   in Block (m, es, indent, sum es 0) end;
   155 
   156 fun markup_block m arg = raw_markup (Markup.output m) arg;
   157 
   158 val blk = markup_block Markup.empty;
   159 fun block prts = blk (2, prts);
   160 val strs = block o breaks o map str;
   161 
   162 fun markup m prts = markup_block m (0, prts);
   163 fun mark m prt = if m = Markup.empty then prt else markup m [prt];
   164 fun mark_str (m, s) = mark m (str s);
   165 fun marks_str (ms, s) = fold_rev mark ms (str s);
   166 
   167 val item = markup Markup.item;
   168 val text_fold = markup Markup.text_fold;
   169 
   170 fun keyword1 name = mark_str (Markup.keyword1, name);
   171 fun keyword2 name = mark_str (Markup.keyword2, name);
   172 
   173 val text = breaks o map str o Symbol.explode_words;
   174 val paragraph = markup Markup.paragraph;
   175 val para = paragraph o text;
   176 
   177 fun quote prt = blk (1, [str "\"", prt, str "\""]);
   178 fun backquote prt = blk (1, [str "`", prt, str "`"]);
   179 fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
   180 
   181 fun separate sep prts =
   182   flat (Library.separate [str sep, brk 1] (map single prts));
   183 
   184 val commas = separate ",";
   185 
   186 fun enclose lpar rpar prts =
   187   block (str lpar :: (prts @ [str rpar]));
   188 
   189 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
   190 
   191 val position =
   192   enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
   193 
   194 val list = enum ",";
   195 fun str_list lpar rpar strs = list lpar rpar (map str strs);
   196 
   197 fun big_list name prts = block (fbreaks (str name :: prts));
   198 
   199 fun indent 0 prt = prt
   200   | indent n prt = blk (0, [str (spaces n), prt]);
   201 
   202 fun unbreakable (Break (_, wd, _)) = String (output_spaces wd, wd)
   203   | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
   204   | unbreakable (e as String _) = e;
   205 
   206 
   207 
   208 (** formatting **)
   209 
   210 (* formatted output *)
   211 
   212 local
   213 
   214 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
   215 
   216 val empty: text =
   217  {tx = Buffer.empty,
   218   ind = Buffer.empty,
   219   pos = 0,
   220   nl = 0};
   221 
   222 fun newline {tx, ind = _, pos = _, nl} : text =
   223  {tx = Buffer.add (Output.output "\n") tx,
   224   ind = Buffer.empty,
   225   pos = 0,
   226   nl = nl + 1};
   227 
   228 fun control s {tx, ind, pos: int, nl} : text =
   229  {tx = Buffer.add s tx,
   230   ind = ind,
   231   pos = pos,
   232   nl = nl};
   233 
   234 fun string (s, len) {tx, ind, pos: int, nl} : text =
   235  {tx = Buffer.add s tx,
   236   ind = Buffer.add s ind,
   237   pos = pos + len,
   238   nl = nl};
   239 
   240 fun blanks wd = string (output_spaces wd, wd);
   241 
   242 fun indentation (buf, len) {tx, ind, pos, nl} : text =
   243   let val s = Buffer.content buf in
   244    {tx = Buffer.add (mode_indent s len) tx,
   245     ind = Buffer.add s ind,
   246     pos = pos + len,
   247     nl = nl}
   248   end;
   249 
   250 (*Add the lengths of the expressions until the next Break; if no Break then
   251   include "after", to account for text following this block.*)
   252 fun breakdist (Break _ :: _, _) = 0
   253   | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
   254   | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
   255   | breakdist ([], after) = after;
   256 
   257 (*Search for the next break (at this or higher levels) and force it to occur.*)
   258 fun forcenext [] = []
   259   | forcenext (Break _ :: es) = fbrk :: es
   260   | forcenext (e :: es) = e :: forcenext es;
   261 
   262 in
   263 
   264 fun formatted margin input =
   265   let
   266     val breakgain = margin div 20;     (*minimum added space required of a break*)
   267     val emergencypos = margin div 2;   (*position too far to right*)
   268 
   269     (*es is list of expressions to print;
   270       blockin is the indentation of the current block;
   271       after is the width of the following context until next break.*)
   272     fun format ([], _, _) text = text
   273       | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
   274           (case e of
   275             Block ((bg, en), bes, indent, _) =>
   276               let
   277                 val pos' = pos + indent;
   278                 val pos'' = pos' mod emergencypos;
   279                 val block' =
   280                   if pos' < emergencypos then (ind |> add_indent indent, pos')
   281                   else (add_indent pos'' Buffer.empty, pos'');
   282                 val btext: text = text
   283                   |> control bg
   284                   |> format (bes, block', breakdist (es, after))
   285                   |> control en;
   286                 (*if this block was broken then force the next break*)
   287                 val es' = if nl < #nl btext then forcenext es else es;
   288               in format (es', block, after) btext end
   289           | Break (force, wd, ind) =>
   290               (*no break if text to next break fits on this line
   291                 or if breaking would add only breakgain to space*)
   292               format (es, block, after)
   293                 (if not force andalso
   294                     pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   295                   then text |> blanks wd  (*just insert wd blanks*)
   296                   else text |> newline |> indentation block |> blanks ind)
   297           | String str => format (es, block, after) (string str text));
   298   in
   299     #tx (format ([input], (Buffer.empty, 0), 0) empty)
   300   end;
   301 
   302 end;
   303 
   304 
   305 (* special output *)
   306 
   307 (*symbolic markup -- no formatting*)
   308 fun symbolic prt =
   309   let
   310     fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
   311       | out (Block ((bg, en), prts, indent, _)) =
   312           Buffer.add bg #>
   313           Buffer.markup (Markup.block indent) (fold out prts) #>
   314           Buffer.add en
   315       | out (String (s, _)) = Buffer.add s
   316       | out (Break (false, wd, ind)) =
   317           Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
   318       | out (Break (true, _, _)) = Buffer.add (Output.output "\n");
   319   in out prt Buffer.empty end;
   320 
   321 (*unformatted output*)
   322 fun unformatted prt =
   323   let
   324     fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
   325       | fmt (String (s, _)) = Buffer.add s
   326       | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd);
   327   in fmt prt Buffer.empty end;
   328 
   329 
   330 (* output interfaces *)
   331 
   332 val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
   333 
   334 val symbolicN = "pretty_symbolic";
   335 
   336 fun output_buffer margin prt =
   337   if print_mode_active symbolicN then symbolic prt
   338   else formatted (the_default (! margin_default) margin) prt;
   339 
   340 val output = Buffer.content oo output_buffer;
   341 fun string_of_margin margin = Output.escape o output (SOME margin);
   342 val string_of = Output.escape o output NONE;
   343 val writeln = Output.writeln o string_of;
   344 
   345 val symbolic_output = Buffer.content o symbolic;
   346 val symbolic_string_of = Output.escape o symbolic_output;
   347 
   348 val str_of = Output.escape o Buffer.content o unformatted;
   349 
   350 
   351 (* chunks *)
   352 
   353 fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
   354 val chunks = markup_chunks Markup.empty;
   355 
   356 fun chunks2 prts =
   357   (case try split_last prts of
   358     NONE => blk (0, [])
   359   | SOME (prefix, last) =>
   360       blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
   361 
   362 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
   363 
   364 fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
   365 
   366 fun writeln_chunks prts =
   367   Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
   368 
   369 fun writeln_chunks2 prts =
   370   (case try split_last prts of
   371     NONE => ()
   372   | SOME (prefix, last) =>
   373       (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
   374         [string_of_text_fold last])
   375       |> Output.writelns);
   376 
   377 
   378 
   379 (** ML toplevel pretty printing **)
   380 
   381 fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   382   | to_ML (String s) = ML_Pretty.String s
   383   | to_ML (Break b) = ML_Pretty.Break b;
   384 
   385 fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
   386   | from_ML (ML_Pretty.String s) = String s
   387   | from_ML (ML_Pretty.Break b) = Break b;
   388 
   389 end;
   390 
   391 end;