src/Pure/General/pretty.ML
author paulson
Mon, 16 May 2005 10:29:15 +0200
changeset 15965 f422f8283491
parent 15570 8d8c70b41bab
child 16714 d9e3ef66b38c
permissions -rw-r--r--
Use of IntInf.int instead of int in most numeric simprocs; avoids integer overflow in SML/NJ
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 6116
diff changeset
     1
(*  Title:      Pure/General/pretty.ML
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
8806
wenzelm
parents: 8456
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
     4
    Author:     Markus Wenzel, TU Munich
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     5
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     6
Generic pretty printing module.
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     7
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     8
Loosely based on
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     9
  D. C. Oppen, "Pretty Printing",
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    10
  ACM Transactions on Programming Languages and Systems (1980), 465-483.
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    11
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    12
The object to be printed is given as a tree with indentation and line
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    13
breaking information.  A "break" inserts a newline if the text until
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    14
the next break is too long to fit on the current line.  After the newline,
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    15
text is indented to the level of the enclosing block.  Normally, if a block
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    16
is broken then all enclosing blocks will also be broken.  Only "inconsistent
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    17
breaks" are provided.
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    18
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    19
The stored length of a block is used in breakdist (to treat each inner block as
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    20
a unit for breaking).
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    21
*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    22
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    23
type pprint_args = (string -> unit) * (int -> unit) * (int -> unit) *
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    24
  (unit -> unit) * (unit -> unit);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    25
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    26
signature PRETTY =
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    27
sig
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    28
  type T
8456
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
    29
  val raw_str: string * real -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    30
  val str: string -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    31
  val brk: int -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    32
  val fbrk: T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    33
  val blk: int * T list -> T
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    34
  val unbreakable: T -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    35
  val quote: T -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    36
  val commas: T list -> T list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    37
  val breaks: T list -> T list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    38
  val fbreaks: T list -> T list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    39
  val block: T list -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    40
  val strs: string list -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    41
  val enclose: string -> string -> T list -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    42
  val list: string -> string -> T list -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    43
  val str_list: string -> string -> string list -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    44
  val big_list: string -> T list -> T
8456
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
    45
  val chunks: T list -> T
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
    46
  val indent: int -> T -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    47
  val string_of: T -> string
14995
318e58f49e8d added output, removed pp_undef;
wenzelm
parents: 14981
diff changeset
    48
  val output: T -> string
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    49
  val writeln: T -> unit
12421
54c06c1f88b8 added writelns;
wenzelm
parents: 10952
diff changeset
    50
  val writelns: T list -> unit
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    51
  val str_of: T -> string
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    52
  val pprint: T -> pprint_args -> unit
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    53
  val setdepth: int -> unit
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    54
  val setmargin: int -> unit
6321
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
    55
  val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    56
  type pp
14972
wenzelm
parents: 14832
diff changeset
    57
  val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    58
  val term: pp -> term -> T
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    59
  val typ: pp -> typ -> T
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    60
  val sort: pp -> sort -> T
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    61
  val classrel: pp -> class list -> T
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    62
  val arity: pp -> arity -> T
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    63
  val string_of_term: pp -> term -> string
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    64
  val string_of_typ: pp -> typ -> string
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    65
  val string_of_sort: pp -> sort -> string
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    66
  val string_of_classrel: pp -> class list -> string
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    67
  val string_of_arity: pp -> arity -> string
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    68
end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    69
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    70
structure Pretty : PRETTY =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    71
struct
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    72
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    73
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    74
(** printing items: compound phrases, strings, and breaks **)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    75
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    76
datatype T =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    77
  Block of T list * int * int |         (*body, indentation, length*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    78
  String of string * int |              (*text, length*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    79
  Break of bool * int;                  (*mandatory flag, width if not taken*);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    80
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
    81
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    82
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    83
(** output text **)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    84
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    85
val output_spaces = Output.output o Symbol.spaces;
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    86
val add_indent = Buffer.add o output_spaces;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    87
fun set_indent wd = Buffer.empty |> add_indent wd;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    88
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    89
val empty =
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    90
 {tx = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    91
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    92
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    93
  nl = 0};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    94
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    95
fun newline {tx, ind, pos, nl} =
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    96
 {tx = Buffer.add (Output.output "\n") tx,
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    97
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    98
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
    99
  nl = nl + 1};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   100
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   101
fun string (s, len) {tx, ind, pos: int, nl} =
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   102
 {tx = Buffer.add s tx,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   103
  ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   104
  pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   105
  nl = nl};
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   106
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   107
fun blanks wd = string (output_spaces wd, wd);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   108
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   109
fun indentation (buf, len) {tx, ind, pos, nl} =
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   110
  let val s = Buffer.content buf in
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   111
   {tx = Buffer.add (Output.indent (s, len)) tx,
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   112
    ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   113
    pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   114
    nl = nl}
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   115
  end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   117
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   118
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   119
(** formatting **)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   120
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   121
(* margin *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   122
6321
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   123
fun make_margin_info m =
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   124
 {margin = m,                   (*right margin, or page width*)
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   125
  breakgain = m div 20,         (*minimum added space required of a break*)
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   126
  emergencypos = m div 2};      (*position too far to right*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   127
6321
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   128
val margin_info = ref (make_margin_info 76);
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   129
fun setmargin m = margin_info := make_margin_info m;
207f518167e8 added strlen_real, setmp_margin;
wenzelm
parents: 6271
diff changeset
   130
fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   131
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   132
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   133
(* format *)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   134
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   135
(*Add the lengths of the expressions until the next Break; if no Break then
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   136
  include "after", to account for text following this block.*)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   137
fun breakdist (Block (_, _, len) :: es, after) = len + breakdist (es, after)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   138
  | breakdist (String (s, len) :: es, after) = len + breakdist (es, after)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   139
  | breakdist (Break _ :: es, after) = 0
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   140
  | breakdist ([], after) = after;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   141
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   142
(*Search for the next break (at this or higher levels) and force it to occur.*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   143
fun forcenext [] = []
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   144
  | forcenext (Break (_, wd) :: es) = Break (true, 0) :: es
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   145
  | forcenext (e :: es) = e :: forcenext es;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   146
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   147
(*es is list of expressions to print;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   148
  blockin is the indentation of the current block;
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   149
  after is the width of the following context until next break.*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   150
fun format ([], _, _) text = text
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   151
  | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   152
      (case e of
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   153
        Block (bes, indent, wd) =>
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   154
          let
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   155
            val {emergencypos, ...} = ! margin_info;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   156
            val pos' = pos + indent;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   157
            val pos'' = pos' mod emergencypos;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   158
            val block' =
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   159
              if pos' < emergencypos then (ind |> add_indent indent, pos')
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   160
              else (set_indent pos'', pos'');
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   161
            val btext = format (bes, block', breakdist (es, after)) text;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   162
            (*if this block was broken then force the next break*)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   163
            val es2 = if nl < #nl btext then forcenext es else es;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   164
          in format (es2, block, after) btext end
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   165
      | String str => format (es, block, after) (string str text)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   166
      | Break (force, wd) =>
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   167
          let val {margin, breakgain, ...} = ! margin_info in
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   168
            (*no break if text to next break fits on this line
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   169
              or if breaking would add only breakgain to space*)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   170
            format (es, block, after)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   171
              (if not force andalso
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   172
                  pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   173
                then text |> blanks wd  (*just insert wd blanks*)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   174
                else text |> newline |> indentation block)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   175
          end);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   176
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   177
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   178
(** Exported functions to create formatting expressions **)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   179
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   180
fun length (Block (_, _, len)) = len
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   181
  | length (String (_, len)) = len
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   182
  | length (Break(_, wd)) = wd;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   183
8456
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
   184
fun raw_str (s, len) = String (s, Real.round len);
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   185
val str = String o apsnd Real.round o Output.output_width;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   186
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   187
fun brk wd = Break (false, wd);
9121
25245986e667 fbrk: 2 if not taken;
wenzelm
parents: 8806
diff changeset
   188
val fbrk = Break (true, 2);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   189
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   190
fun blk (indent, es) =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   191
  let
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   192
    fun sum([], k) = k
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   193
      | sum(e :: es, k) = sum (es, length e + k);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   194
  in Block (es, indent, sum (es, 0)) end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   195
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   196
fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   197
  | unbreakable (Block (es, indent, wd)) = Block (map unbreakable es, indent, wd)
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   198
  | unbreakable (e as String _) = e;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   199
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   200
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   201
(* utils *)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   202
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   203
fun quote prt =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   204
  blk (1, [str "\"", prt, str "\""]);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   205
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   206
fun commas prts =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 14995
diff changeset
   207
  List.concat (separate [str ",", brk 1] (map (fn x => [x]) prts));
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   208
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   209
fun breaks prts = separate (brk 1) prts;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   210
fun fbreaks prts = separate fbrk prts;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   211
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   212
fun block prts = blk (2, prts);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   213
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
   214
val strs = block o breaks o map str;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   215
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   216
fun enclose lpar rpar prts =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   217
  block (str lpar :: (prts @ [str rpar]));
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   218
8456
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
   219
fun list lpar rpar prts = enclose lpar rpar (commas prts);
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
   220
fun str_list lpar rpar strs = list lpar rpar (map str strs);
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
   221
fun big_list name prts = block (fbreaks (str name :: prts));
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
   222
fun chunks prts = blk (0, fbreaks prts);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   223
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
   224
fun indent 0 prt = prt
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   225
  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
   226
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   227
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   228
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   229
(** Pretty printing with depth limitation **)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   230
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   231
val depth       = ref 0;        (*maximum depth; 0 means no limit*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   232
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   233
fun setdepth dp = (depth := dp);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   234
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   235
(*Recursively prune blocks, discarding all text exceeding depth dp*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   236
fun pruning dp (Block(bes,indent,wd)) =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   237
      if dp>0 then blk(indent, map (pruning(dp-1)) bes)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   238
              else str "..."
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   239
  | pruning dp e = e;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   240
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   241
fun prune dp e = if dp > 0 then pruning dp e else e;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   242
14995
318e58f49e8d added output, removed pp_undef;
wenzelm
parents: 14981
diff changeset
   243
fun output e =
318e58f49e8d added output, removed pp_undef;
wenzelm
parents: 14981
diff changeset
   244
  Buffer.content (#tx (format ([prune (! depth) e], (Buffer.empty, 0), 0) empty));
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   245
14995
318e58f49e8d added output, removed pp_undef;
wenzelm
parents: 14981
diff changeset
   246
val string_of = Output.raw o output;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   247
val writeln = writeln o string_of;
12421
54c06c1f88b8 added writelns;
wenzelm
parents: 10952
diff changeset
   248
fun writelns [] = () | writelns es = writeln (chunks es);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   249
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   250
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   251
(*Create a single flat string: no line breaking*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   252
fun str_of prt =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   253
  let
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   254
    fun s_of (Block (prts, _, _)) = implode (map s_of prts)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   255
      | s_of (String (s, _)) = s
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   256
      | s_of (Break (false, wd)) = output_spaces wd
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   257
      | s_of (Break (true, _)) = output_spaces 1;
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   258
  in Output.raw (s_of (prune (! depth) prt)) end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   259
8456
8ccda76f07cb removed lst, strlen, strlen_real, spc, sym;
wenzelm
parents: 6321
diff changeset
   260
(*part of the interface to the ML toplevel pretty printers*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   261
fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   262
  let
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   263
    fun pp (Block (prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   264
      | pp (String (s, _)) = put_str s
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   265
      | pp (Break (false, wd)) = put_brk wd
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   266
      | pp (Break (true, _)) = put_fbrk ()
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   267
    and pp_lst [] = ()
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   268
      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   269
  in
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   270
    pp (prune (! depth) prt)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   271
  end;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   272
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   273
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   274
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   275
(** abstract pretty printing context **)
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   276
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   277
datatype pp =
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   278
  PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   279
14972
wenzelm
parents: 14832
diff changeset
   280
val pp = PP;
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   281
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   282
fun pp_fun f (PP x) = f x;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   283
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   284
val term     = pp_fun #1;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   285
val typ      = pp_fun #2;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   286
val sort     = pp_fun #3;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   287
val classrel = pp_fun #4;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   288
val arity    = pp_fun #5;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   289
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   290
val string_of_term     = string_of oo term;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   291
val string_of_typ      = string_of oo typ;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   292
val string_of_sort     = string_of oo sort;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   293
val string_of_classrel = string_of oo classrel;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   294
val string_of_arity    = string_of oo arity;
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   295
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   296
end;