pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
authorwenzelm
Sat May 29 15:05:51 2004 +0200 (2004-05-29)
changeset 148326589a58f57cb
parent 14831 7c37c18a6188
child 14833 30556b84af7c
pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Sat May 29 15:05:37 2004 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Sat May 29 15:05:51 2004 +0200
     1.3 @@ -25,13 +25,14 @@
     1.4    (unit -> unit) * (unit -> unit);
     1.5  
     1.6  signature PRETTY =
     1.7 -  sig
     1.8 +sig
     1.9    type T
    1.10    val raw_str: string * real -> T
    1.11    val str: string -> T
    1.12    val brk: int -> T
    1.13    val fbrk: T
    1.14    val blk: int * T list -> T
    1.15 +  val unbreakable: T -> T
    1.16    val quote: T -> T
    1.17    val commas: T list -> T list
    1.18    val breaks: T list -> T list
    1.19 @@ -52,7 +53,21 @@
    1.20    val setdepth: int -> unit
    1.21    val setmargin: int -> unit
    1.22    val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    1.23 -  end;
    1.24 +  type pp
    1.25 +  val pp: (term -> T) -> (typ -> T) -> (sort -> T) ->
    1.26 +    (class list -> T) -> (arity -> T)  -> pp
    1.27 +  val pp_undef: pp
    1.28 +  val term: pp -> term -> T
    1.29 +  val typ: pp -> typ -> T
    1.30 +  val sort: pp -> sort -> T
    1.31 +  val classrel: pp -> class list -> T
    1.32 +  val arity: pp -> arity -> T
    1.33 +  val string_of_term: pp -> term -> string
    1.34 +  val string_of_typ: pp -> typ -> string
    1.35 +  val string_of_sort: pp -> sort -> string
    1.36 +  val string_of_classrel: pp -> class list -> string
    1.37 +  val string_of_arity: pp -> arity -> string
    1.38 +end;
    1.39  
    1.40  structure Pretty : PRETTY =
    1.41  struct
    1.42 @@ -69,7 +84,7 @@
    1.43  
    1.44  (** output text **)
    1.45  
    1.46 -val output_spaces = Symbol.output o Symbol.spaces;
    1.47 +val output_spaces = Output.output o Symbol.spaces;
    1.48  val add_indent = Buffer.add o output_spaces;
    1.49  fun set_indent wd = Buffer.empty |> add_indent wd;
    1.50  
    1.51 @@ -80,7 +95,7 @@
    1.52    nl = 0};
    1.53  
    1.54  fun newline {tx, ind, pos, nl} =
    1.55 - {tx = Buffer.add (Symbol.output "\n") tx,
    1.56 + {tx = Buffer.add (Output.output "\n") tx,
    1.57    ind = Buffer.empty,
    1.58    pos = 0,
    1.59    nl = nl + 1};
    1.60 @@ -95,7 +110,7 @@
    1.61  
    1.62  fun indentation (buf, len) {tx, ind, pos, nl} =
    1.63    let val s = Buffer.content buf in
    1.64 -   {tx = Buffer.add (Symbol.indent (s, len)) tx,
    1.65 +   {tx = Buffer.add (Output.indent (s, len)) tx,
    1.66      ind = Buffer.add s ind,
    1.67      pos = pos + len,
    1.68      nl = nl}
    1.69 @@ -162,14 +177,14 @@
    1.70            end);
    1.71  
    1.72  
    1.73 -(*** Exported functions to create formatting expressions ***)
    1.74 +(** Exported functions to create formatting expressions **)
    1.75  
    1.76  fun length (Block (_, _, len)) = len
    1.77    | length (String (_, len)) = len
    1.78    | length (Break(_, wd)) = wd;
    1.79  
    1.80  fun raw_str (s, len) = String (s, Real.round len);
    1.81 -val str = String o apsnd Real.round o Symbol.output_width;
    1.82 +val str = String o apsnd Real.round o Output.output_width;
    1.83  
    1.84  fun brk wd = Break (false, wd);
    1.85  val fbrk = Break (true, 2);
    1.86 @@ -180,6 +195,10 @@
    1.87        | sum(e :: es, k) = sum (es, length e + k);
    1.88    in Block (es, indent, sum (es, 0)) end;
    1.89  
    1.90 +fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
    1.91 +  | unbreakable (Block (es, indent, wd)) = Block (map unbreakable es, indent, wd)
    1.92 +  | unbreakable (e as String _) = e;
    1.93 +
    1.94  
    1.95  (* utils *)
    1.96  
    1.97 @@ -208,7 +227,8 @@
    1.98    | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
    1.99  
   1.100  
   1.101 -(*** Pretty printing with depth limitation ***)
   1.102 +
   1.103 +(** Pretty printing with depth limitation **)
   1.104  
   1.105  val depth       = ref 0;        (*maximum depth; 0 means no limit*)
   1.106  
   1.107 @@ -222,7 +242,10 @@
   1.108  
   1.109  fun prune dp e = if dp > 0 then pruning dp e else e;
   1.110  
   1.111 -fun string_of e = Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
   1.112 +fun string_of e =
   1.113 +  Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty))
   1.114 +  |> Output.raw;
   1.115 +
   1.116  val writeln = writeln o string_of;
   1.117  fun writelns [] = () | writelns es = writeln (chunks es);
   1.118  
   1.119 @@ -234,7 +257,7 @@
   1.120        | s_of (String (s, _)) = s
   1.121        | s_of (Break (false, wd)) = output_spaces wd
   1.122        | s_of (Break (true, _)) = output_spaces 1;
   1.123 -  in s_of (prune (! depth) prt) end;
   1.124 +  in Output.raw (s_of (prune (! depth) prt)) end;
   1.125  
   1.126  (*part of the interface to the ML toplevel pretty printers*)
   1.127  fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
   1.128 @@ -250,4 +273,30 @@
   1.129    end;
   1.130  
   1.131  
   1.132 +
   1.133 +(** abstract pretty printing context **)
   1.134 +
   1.135 +datatype pp =
   1.136 +  PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
   1.137 +
   1.138 +fun pp f1 f2 f3 f4 f5 = PP (f1, f2, f3, f4, f5);
   1.139 +
   1.140 +fun pp_fun f (PP x) = f x;
   1.141 +
   1.142 +val term     = pp_fun #1;
   1.143 +val typ      = pp_fun #2;
   1.144 +val sort     = pp_fun #3;
   1.145 +val classrel = pp_fun #4;
   1.146 +val arity    = pp_fun #5;
   1.147 +
   1.148 +val string_of_term     = string_of oo term;
   1.149 +val string_of_typ      = string_of oo typ;
   1.150 +val string_of_sort     = string_of oo sort;
   1.151 +val string_of_classrel = string_of oo classrel;
   1.152 +val string_of_arity    = string_of oo arity;
   1.153 +
   1.154 +fun undef kind _ = str ("*** UNABLE TO PRINT " ^ kind ^ " ***");
   1.155 +val pp_undef =
   1.156 +  pp (undef "term") (undef "typ") (undef "sort") (undef "classrel") (undef "arity");
   1.157 +
   1.158  end;