(*  Title:      Pure/General/pretty.ML

     ID:         $Id$

     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     Author:     Markus Wenzel, TU Munich

 Generic 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).

 *)

 type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *

   (unit -> unit) * (unit -> unit);

 signature PRETTY =

 sig

   val default_indent: string -> int -> string

   val default_markup: Markup.T -> string * string

   val add_mode: string -> (string -> int -> string) -> (Markup.T -> string * string) -> unit

   type T

   val raw_str: string * int -> T

   val str: string -> T

   val brk: int -> T

   val fbrk: T

   val blk: int * T list -> T

   val unbreakable: T -> T

   val breaks: T list -> T list

   val fbreaks: T list -> T list

   val block: T list -> T

   val markup: Markup.T -> T list -> T

   val keyword: string -> T

   val command: string -> T

   val strs: string list -> T

   val chunks: T list -> T

   val chunks2: T list -> T

   val block_enclose: T * T -> T list -> T

   val quote: T -> T

   val backquote: T -> T

   val separate: string -> T list -> T list

   val commas: T list -> T list

   val enclose: string -> string -> T list -> T

   val enum: string -> string -> string -> T list -> T

   val list: string -> string -> T list -> T

   val str_list: string -> string -> string list -> T

   val big_list: string -> T list -> T

   val indent: int -> T -> T

   val string_of: T -> string

   val output_buffer: T -> Buffer.T

   val output: T -> string

   val writeln: T -> unit

   val str_of: T -> string

   val pprint: T -> pprint_args -> unit

   val setdepth: int -> unit

   val setmargin: int -> unit

   val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b

   type pp

   val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp

   val term: pp -> term -> T

   val typ: pp -> typ -> T

   val sort: pp -> sort -> T

   val classrel: pp -> class list -> T

   val arity: pp -> arity -> T

   val string_of_term: pp -> term -> string

   val string_of_typ: pp -> typ -> string

   val string_of_sort: pp -> sort -> string

   val string_of_classrel: pp -> class list -> string

   val string_of_arity: pp -> arity -> string

 end;

 structure Pretty: PRETTY =

 struct

 (** print mode operations **)

 fun default_indent (_: string) = Symbol.spaces;

 fun default_markup (_: Markup.T) = ("", "");

 local

   val default = {indent = default_indent, markup = default_markup};

   val modes = ref (Symtab.make [("", default)]);

 in

   fun add_mode name indent markup =

     change modes (Symtab.update_new (name, {indent = indent, markup = markup}));

   fun get_mode () =

     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));

 end;

 fun mode_indent x y = #indent (get_mode ()) x y;

 fun mode_markup x = #markup (get_mode ()) x;

 (** printing items: compound phrases, strings, and breaks **)

 datatype T =

   Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)

   String of string * int |                  (*text, length*)

   Break of bool * int;                      (*mandatory flag, width if not taken*)

 (** output text **)

 val output_spaces = Output.output o Symbol.spaces;

 val add_indent = Buffer.add o output_spaces;

 fun set_indent wd = Buffer.empty |> add_indent wd;

 type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};

 val empty: text =

  {tx = Buffer.empty,

   ind = Buffer.empty,

   pos = 0,

   nl = 0};

 fun newline {tx, ind, pos, nl} : text =

  {tx = Buffer.add (Output.output "\n") tx,

   ind = Buffer.empty,

   pos = 0,

   nl = nl + 1};

 fun string (s, len) {tx, ind, pos: int, nl} : text =

  {tx = Buffer.add s tx,

   ind = Buffer.add s ind,

   pos = pos + len,

   nl = nl};

 fun blanks wd = string (output_spaces wd, wd);

 fun indentation (buf, len) {tx, ind, pos, nl} : text =

   let val s = Buffer.content buf in

    {tx = Buffer.add (mode_indent s len) tx,

     ind = Buffer.add s ind,

     pos = pos + len,

     nl = nl}

   end;

 (** formatting **)

 (* margin *)

 fun make_margin_info m =

  {margin = m,                   (*right margin, or page width*)

   breakgain = m div 20,         (*minimum added space required of a break*)

   emergencypos = m div 2};      (*position too far to right*)

 val margin_info = ref (make_margin_info 76);

 fun setmargin m = margin_info := make_margin_info m;

 fun setmp_margin m f = setmp margin_info (make_margin_info m) f;

 (* format *)

 (*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, len) :: es, after) = len + breakdist (es, after)

   | breakdist (Break _ :: es, after) = 0

   | breakdist ([], after) = after;

 (*Search for the next break (at this or higher levels) and force it to occur.*)

 fun forcenext [] = []

   | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es

   | forcenext (e :: es) = e :: forcenext es;

 (*es is list of expressions to print;

   blockin is the indentation of the current block;

   after is the width of the following context until next break.*)

 fun format ([], _, _) text = text

   | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =

       (case e of

         Block (markup, bes, indent, wd) =>

           let

             val {emergencypos, ...} = ! margin_info;

             val pos' = pos + indent;

             val pos'' = pos' mod emergencypos;

             val block' =

               if pos' < emergencypos then (ind |> add_indent indent, pos')

               else (set_indent pos'', pos'');

             val (bg, en) = if markup = Markup.none then ("", "") else mode_markup markup;

             val btext: text = text

               |> string (bg, 0)

               |> format (bes, block', breakdist (es, after))

               |> string (en, 0);

             (*if this block was broken then force the next break*)

             val es' = if nl < #nl btext then forcenext es else es;

           in format (es', block, after) btext end

       | String str => format (es, block, after) (string str text)

       | Break (force, wd) =>

           let val {margin, breakgain, ...} = ! margin_info in

             (*no break if text to next break fits on this line

               or if breaking would add only breakgain to space*)

             format (es, block, after)

               (if not force andalso

                   pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)

                 then text |> blanks wd  (*just insert wd blanks*)

                 else text |> newline |> indentation block)

           end);

 (** Exported functions to create formatting expressions **)

 fun length (Block (_, _, _, len)) = len

   | length (String (_, len)) = len

   | length (Break(_, wd)) = wd;

 val raw_str = String;

 val str = String o Output.output_width;

 fun brk wd = Break (false, wd);

 val fbrk = Break (true, 2);

 fun markup_block m (indent, es) =

   let

     fun sum [] k = k

       | sum (e :: es) k = sum es (length e + k);

   in Block (m, es, indent, sum es 0) end;

 val blk = markup_block Markup.none;

 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)

   | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)

   | unbreakable (e as String _) = e;

 (* utils *)

 fun breaks prts = Library.separate (brk 1) prts;

 fun fbreaks prts = Library.separate fbrk prts;

 fun block prts = blk (2, prts);

 fun markup m prts = markup_block m (0, prts);

 fun keyword name = markup (Markup.keyword name) [str name];

 fun command name = markup (Markup.command name) [str name];

 val strs = block o breaks o map str;

 fun chunks prts = blk (0, fbreaks prts);

 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));

 fun block_enclose (p1, p2) ps = chunks [(block  o fbreaks) (p1 :: ps), p2];

 fun quote prt = blk (1, [str "\"", prt, str "\""]);

 fun backquote prt = blk (1, [str "`", prt, str "`"]);

 fun separate sep prts =

   flat (Library.separate [str sep, brk 1] (map single prts));

 val commas = separate ",";

 fun enclose lpar rpar prts =

   block (str lpar :: (prts @ [str rpar]));

 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);

 val list = enum ",";

 fun str_list lpar rpar strs = list lpar rpar (map str strs);

 fun big_list name prts = block (fbreaks (str name :: prts));

 fun indent 0 prt = prt

   | indent n prt = blk (0, [str (Symbol.spaces n), prt]);

 (** Pretty printing with depth limitation **)

 val depth       = ref 0;        (*maximum depth; 0 means no limit*)

 fun setdepth dp = (depth := dp);

 (*Recursively prune blocks, discarding all text exceeding depth dp*)

 fun pruning dp (Block (m, bes, indent, wd)) =

       if dp > 0

       then markup_block m (indent, map (pruning (dp - 1)) bes)

       else str "..."

   | pruning dp e = e;

 fun prune dp e = if dp > 0 then pruning dp e else e;

 fun output_buffer e = #tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty);

 val output = Buffer.content o output_buffer;

 val string_of = Output.escape o output;

 val writeln = Output.writeln o string_of;

 (*Create a single flat string: no line breaking*)

 fun str_of prt =

   let

     fun fmt (Block (m, prts, _, _)) =

           let val (bg, en) = mode_markup m

           in Buffer.add bg #> fold fmt prts #> Buffer.add en end

       | fmt (String (s, _)) = Buffer.add s

       | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)

       | fmt (Break (true, _)) = Buffer.add (output_spaces 1);

   in Output.escape (Buffer.content (fmt (prune (! depth) prt) Buffer.empty)) end;

 (*part of the interface to the ML toplevel pretty printers*)

 fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =

   let

     fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())

       | pp (String (s, _)) = put_str s

       | pp (Break (false, wd)) = put_brk wd

       | pp (Break (true, _)) = put_fbrk ()

     and pp_lst [] = ()

       | pp_lst (prt :: prts) = (pp prt; pp_lst prts);

   in pp (prune (! depth) prt) end;

 (** abstract pretty printing context **)

 datatype pp =

   PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);

 val pp = PP;

 fun pp_fun f (PP x) = f x;

 val term     = pp_fun #1;

 val typ      = pp_fun #2;

 val sort     = pp_fun #3;

 val classrel = pp_fun #4;

 val arity    = pp_fun #5;

 val string_of_term     = string_of oo term;

 val string_of_typ      = string_of oo typ;

 val string_of_sort     = string_of oo sort;

 val string_of_classrel = string_of oo classrel;

 val string_of_arity    = string_of oo arity;

 end;