src/Pure/General/pretty.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 43684 85388f5570c4
child 45666 d83797ef0d2d
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     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 default_indent: string -> int -> Output.output
    25   val add_mode: string -> (string -> int -> Output.output) -> unit
    26   type T
    27   val str: string -> T
    28   val brk: int -> T
    29   val fbrk: T
    30   val breaks: T list -> T list
    31   val fbreaks: T list -> T list
    32   val blk: int * T list -> T
    33   val block: T list -> T
    34   val strs: string list -> T
    35   val markup: Markup.T -> T list -> T
    36   val mark: Markup.T -> T -> T
    37   val mark_str: Markup.T * string -> T
    38   val marks_str: Markup.T list * string -> T
    39   val keyword: string -> T
    40   val command: string -> T
    41   val markup_chunks: Markup.T -> T list -> T
    42   val chunks: T list -> T
    43   val chunks2: T list -> T
    44   val block_enclose: T * T -> T list -> T
    45   val quote: T -> T
    46   val backquote: T -> T
    47   val separate: string -> T list -> T list
    48   val commas: T list -> T list
    49   val enclose: string -> string -> T list -> T
    50   val enum: string -> string -> string -> T list -> T
    51   val position: Position.T -> T
    52   val list: string -> string -> T list -> T
    53   val str_list: string -> string -> string list -> T
    54   val big_list: string -> T list -> T
    55   val indent: int -> T -> T
    56   val unbreakable: T -> T
    57   val margin_default: int Unsynchronized.ref
    58   val symbolicN: string
    59   val output_buffer: int option -> T -> Buffer.T
    60   val output: int option -> T -> Output.output
    61   val string_of_margin: int -> T -> string
    62   val string_of: T -> string
    63   val str_of: T -> string
    64   val writeln: T -> unit
    65   val to_ML: T -> ML_Pretty.pretty
    66   val from_ML: ML_Pretty.pretty -> T
    67 end;
    68 
    69 structure Pretty: PRETTY =
    70 struct
    71 
    72 (** print mode operations **)
    73 
    74 fun default_indent (_: string) = Symbol.spaces;
    75 
    76 local
    77   val default = {indent = default_indent};
    78   val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
    79 in
    80   fun add_mode name indent =
    81     Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
    82   fun get_mode () =
    83     the_default default
    84       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    85 end;
    86 
    87 fun mode_indent x y = #indent (get_mode ()) x y;
    88 
    89 val output_spaces = Output.output o Symbol.spaces;
    90 val add_indent = Buffer.add o output_spaces;
    91 
    92 
    93 
    94 (** printing items: compound phrases, strings, and breaks **)
    95 
    96 abstype T =
    97     Block of (Output.output * Output.output) * T list * int * int
    98       (*markup output, body, indentation, length*)
    99   | String of Output.output * int  (*text, length*)
   100   | Break of bool * int  (*mandatory flag, width if not taken*)
   101 with
   102 
   103 fun length (Block (_, _, _, len)) = len
   104   | length (String (_, len)) = len
   105   | length (Break (_, wd)) = wd;
   106 
   107 
   108 
   109 (** derived operations to create formatting expressions **)
   110 
   111 val str = String o Output.output_width;
   112 
   113 fun brk wd = Break (false, wd);
   114 val fbrk = Break (true, 1);
   115 
   116 fun breaks prts = Library.separate (brk 1) prts;
   117 fun fbreaks prts = Library.separate fbrk prts;
   118 
   119 fun block_markup m (indent, es) =
   120   let
   121     fun sum [] k = k
   122       | sum (e :: es) k = sum es (length e + k);
   123   in Block (m, es, indent, sum es 0) end;
   124 
   125 fun markup_block m arg = block_markup (Markup.output m) arg;
   126 
   127 val blk = markup_block Markup.empty;
   128 fun block prts = blk (2, prts);
   129 val strs = block o breaks o map str;
   130 
   131 fun markup m prts = markup_block m (0, prts);
   132 fun mark m prt = if m = Markup.empty then prt else markup m [prt];
   133 fun mark_str (m, s) = mark m (str s);
   134 fun marks_str (ms, s) = fold_rev mark ms (str s);
   135 
   136 fun keyword name = mark_str (Markup.keyword, name);
   137 fun command name = mark_str (Markup.command, name);
   138 
   139 fun markup_chunks m prts = markup m (fbreaks prts);
   140 val chunks = markup_chunks Markup.empty;
   141 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
   142 
   143 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
   144 
   145 fun quote prt = blk (1, [str "\"", prt, str "\""]);
   146 fun backquote prt = blk (1, [str "`", prt, str "`"]);
   147 
   148 fun separate sep prts =
   149   flat (Library.separate [str sep, brk 1] (map single prts));
   150 
   151 val commas = separate ",";
   152 
   153 fun enclose lpar rpar prts =
   154   block (str lpar :: (prts @ [str rpar]));
   155 
   156 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
   157 
   158 val position =
   159   enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
   160 
   161 val list = enum ",";
   162 fun str_list lpar rpar strs = list lpar rpar (map str strs);
   163 
   164 fun big_list name prts = block (fbreaks (str name :: prts));
   165 
   166 fun indent 0 prt = prt
   167   | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
   168 
   169 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
   170   | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
   171   | unbreakable (e as String _) = e;
   172 
   173 
   174 
   175 (** formatting **)
   176 
   177 (* formatted output *)
   178 
   179 local
   180 
   181 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
   182 
   183 val empty: text =
   184  {tx = Buffer.empty,
   185   ind = Buffer.empty,
   186   pos = 0,
   187   nl = 0};
   188 
   189 fun newline {tx, ind = _, pos = _, nl} : text =
   190  {tx = Buffer.add (Output.output "\n") tx,
   191   ind = Buffer.empty,
   192   pos = 0,
   193   nl = nl + 1};
   194 
   195 fun control s {tx, ind, pos: int, nl} : text =
   196  {tx = Buffer.add s tx,
   197   ind = ind,
   198   pos = pos,
   199   nl = nl};
   200 
   201 fun string (s, len) {tx, ind, pos: int, nl} : text =
   202  {tx = Buffer.add s tx,
   203   ind = Buffer.add s ind,
   204   pos = pos + len,
   205   nl = nl};
   206 
   207 fun blanks wd = string (output_spaces wd, wd);
   208 
   209 fun indentation (buf, len) {tx, ind, pos, nl} : text =
   210   let val s = Buffer.content buf in
   211    {tx = Buffer.add (mode_indent s len) tx,
   212     ind = Buffer.add s ind,
   213     pos = pos + len,
   214     nl = nl}
   215   end;
   216 
   217 (*Add the lengths of the expressions until the next Break; if no Break then
   218   include "after", to account for text following this block.*)
   219 fun breakdist (Break _ :: _, _) = 0
   220   | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
   221   | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
   222   | breakdist ([], after) = after;
   223 
   224 (*Search for the next break (at this or higher levels) and force it to occur.*)
   225 fun forcenext [] = []
   226   | forcenext (Break _ :: es) = fbrk :: es
   227   | forcenext (e :: es) = e :: forcenext es;
   228 
   229 in
   230 
   231 fun formatted margin input =
   232   let
   233     val breakgain = margin div 20;     (*minimum added space required of a break*)
   234     val emergencypos = margin div 2;   (*position too far to right*)
   235 
   236     (*es is list of expressions to print;
   237       blockin is the indentation of the current block;
   238       after is the width of the following context until next break.*)
   239     fun format ([], _, _) text = text
   240       | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
   241           (case e of
   242             Block ((bg, en), bes, indent, _) =>
   243               let
   244                 val pos' = pos + indent;
   245                 val pos'' = pos' mod emergencypos;
   246                 val block' =
   247                   if pos' < emergencypos then (ind |> add_indent indent, pos')
   248                   else (add_indent pos'' Buffer.empty, pos'');
   249                 val btext: text = text
   250                   |> control bg
   251                   |> format (bes, block', breakdist (es, after))
   252                   |> control en;
   253                 (*if this block was broken then force the next break*)
   254                 val es' = if nl < #nl btext then forcenext es else es;
   255               in format (es', block, after) btext end
   256           | Break (force, wd) =>
   257               (*no break if text to next break fits on this line
   258                 or if breaking would add only breakgain to space*)
   259               format (es, block, after)
   260                 (if not force andalso
   261                     pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
   262                   then text |> blanks wd  (*just insert wd blanks*)
   263                   else text |> newline |> indentation block)
   264           | String str => format (es, block, after) (string str text));
   265   in
   266     #tx (format ([input], (Buffer.empty, 0), 0) empty)
   267   end;
   268 
   269 end;
   270 
   271 
   272 (* special output *)
   273 
   274 (*symbolic markup -- no formatting*)
   275 fun symbolic prt =
   276   let
   277     fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
   278       | out (Block ((bg, en), prts, indent, _)) =
   279           Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
   280       | out (String (s, _)) = Buffer.add s
   281       | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
   282       | out (Break (true, _)) = Buffer.add (Output.output "\n");
   283   in out prt Buffer.empty end;
   284 
   285 (*unformatted output*)
   286 fun unformatted prt =
   287   let
   288     fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
   289       | fmt (String (s, _)) = Buffer.add s
   290       | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
   291   in fmt prt Buffer.empty end;
   292 
   293 
   294 (* output interfaces *)
   295 
   296 val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
   297 
   298 val symbolicN = "pretty_symbolic";
   299 
   300 fun output_buffer margin prt =
   301   if print_mode_active symbolicN then symbolic prt
   302   else formatted (the_default (! margin_default) margin) prt;
   303 
   304 val output = Buffer.content oo output_buffer;
   305 fun string_of_margin margin = Output.escape o output (SOME margin);
   306 val string_of = Output.escape o output NONE;
   307 val str_of = Output.escape o Buffer.content o unformatted;
   308 val writeln = Output.writeln o string_of;
   309 
   310 
   311 
   312 (** ML toplevel pretty printing **)
   313 
   314 fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   315   | to_ML (String s) = ML_Pretty.String s
   316   | to_ML (Break b) = ML_Pretty.Break b;
   317 
   318 fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
   319   | from_ML (ML_Pretty.String s) = String s
   320   | from_ML (ML_Pretty.Break b) = Break b;
   321 
   322 end;
   323 
   324 end;