src/Pure/General/pretty.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24612 d1b315bdb8d7
child 26703 c07b1a90600c
permissions -rw-r--r--
filtering out some package theorems
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
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23659
diff changeset
    23
type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
6116
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
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23659
diff changeset
    28
  val default_indent: string -> int -> output
23698
af84f2f13d4d moved print_mode setup for markup to markup.ML;
wenzelm
parents: 23660
diff changeset
    29
  val add_mode: string -> (string -> int -> output) -> unit
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    30
  type T
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23659
diff changeset
    31
  val raw_str: output * int -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    32
  val str: string -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    33
  val brk: int -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    34
  val fbrk: T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    35
  val breaks: T list -> T list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    36
  val fbreaks: T list -> T list
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    37
  val blk: int * T list -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    38
  val block: T list -> T
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    39
  val strs: string list -> T
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    40
  val markup: Markup.T -> T list -> T
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    41
  val keyword: string -> T
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    42
  val command: string -> T
23638
09120c2dd71f added markup_chunks;
wenzelm
parents: 23628
diff changeset
    43
  val markup_chunks: Markup.T -> T list -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    44
  val chunks: T list -> T
19266
2e8ad3f2cd66 added command, keyword;
wenzelm
parents: 18802
diff changeset
    45
  val chunks2: T list -> T
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    46
  val block_enclose: T * T -> T list -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    47
  val quote: T -> T
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    48
  val backquote: T -> T
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    49
  val separate: string -> T list -> T list
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    50
  val commas: T list -> T list
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    51
  val enclose: string -> string -> T list -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    52
  val enum: string -> string -> string -> T list -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    53
  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
    54
  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
    55
  val big_list: string -> T list -> T
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
    56
  val indent: int -> T -> T
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    57
  val unbreakable: T -> T
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    58
  val setmargin: int -> unit
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    59
  val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    60
  val setdepth: int -> unit
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    61
  val pprint: T -> pprint_args -> unit
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    62
  val symbolicN: string
16714
d9e3ef66b38c added output_buffer;
wenzelm
parents: 15570
diff changeset
    63
  val output_buffer: T -> Buffer.T
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23659
diff changeset
    64
  val output: T -> output
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    65
  val string_of: T -> string
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    66
  val str_of: T -> string
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    67
  val writeln: T -> unit
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
    68
  type pp
14972
wenzelm
parents: 14832
diff changeset
    69
  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
    70
  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
    71
  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
    72
  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
    73
  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
    74
  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
    75
  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
    76
  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
    77
  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
    78
  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
    79
  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
    80
end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    81
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    82
structure Pretty: PRETTY =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    83
struct
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    84
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    85
(** print mode operations **)
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    86
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    87
fun default_indent (_: string) = Symbol.spaces;
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    88
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    89
local
23698
af84f2f13d4d moved print_mode setup for markup to markup.ML;
wenzelm
parents: 23660
diff changeset
    90
  val default = {indent = default_indent};
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    91
  val modes = ref (Symtab.make [("", default)]);
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    92
in
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23787
diff changeset
    93
  fun add_mode name indent = CRITICAL (fn () =>
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23787
diff changeset
    94
    change modes (Symtab.update_new (name, {indent = indent})));
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    95
  fun get_mode () =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 23922
diff changeset
    96
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    97
end;
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    98
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    99
fun mode_indent x y = #indent (get_mode ()) x y;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   100
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   101
val output_spaces = Output.output o Symbol.spaces;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   102
val add_indent = Buffer.add o output_spaces;
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   103
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   104
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   105
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   106
(** printing items: compound phrases, strings, and breaks **)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   107
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   108
datatype T =
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   109
  Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23659
diff changeset
   110
  String of output * int |                  (*text, length*)
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   111
  Break of bool * int;                      (*mandatory flag, width if not taken*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   112
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   113
fun length (Block (_, _, _, len)) = len
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   114
  | length (String (_, len)) = len
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   115
  | length (Break (_, wd)) = wd;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   116
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
   117
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   118
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   119
(** derived operations to create formatting expressions **)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   120
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   121
val raw_str = String;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   122
val str = String o Output.output_width;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   123
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   124
fun brk wd = Break (false, wd);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   125
val fbrk = Break (true, 2);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   126
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   127
fun breaks prts = Library.separate (brk 1) prts;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   128
fun fbreaks prts = Library.separate fbrk prts;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   129
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   130
fun markup_block m (indent, es) =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   131
  let
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   132
    fun sum [] k = k
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   133
      | sum (e :: es) k = sum es (length e + k);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   134
  in Block (m, es, indent, sum es 0) end;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   135
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   136
val blk = markup_block Markup.none;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   137
fun block prts = blk (2, prts);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   138
val strs = block o breaks o map str;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   139
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   140
fun markup m prts = markup_block m (0, prts);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   141
fun keyword name = markup (Markup.keyword name) [str name];
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   142
fun command name = markup (Markup.command name) [str name];
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   143
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   144
fun markup_chunks m prts = markup m (fbreaks prts);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   145
val chunks = markup_chunks Markup.none;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   146
fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   147
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   148
fun block_enclose (p1, p2) ps = chunks [(block  o fbreaks) (p1 :: ps), p2];
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   149
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   150
fun quote prt = blk (1, [str "\"", prt, str "\""]);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   151
fun backquote prt = blk (1, [str "`", prt, str "`"]);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   152
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   153
fun separate sep prts =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   154
  flat (Library.separate [str sep, brk 1] (map single prts));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   155
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   156
val commas = separate ",";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   157
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   158
fun enclose lpar rpar prts =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   159
  block (str lpar :: (prts @ [str rpar]));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   160
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   161
fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   162
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   163
val list = enum ",";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   164
fun str_list lpar rpar strs = list lpar rpar (map str strs);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   165
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   166
fun big_list name prts = block (fbreaks (str name :: prts));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   167
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   168
fun indent 0 prt = prt
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   169
  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   170
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   171
fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   172
  | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   173
  | unbreakable (e as String _) = e;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   174
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   175
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   176
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   177
(** formatting **)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   178
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   179
(* margin *)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   180
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   181
fun make_margin_info m =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   182
 {margin = m,                   (*right margin, or page width*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   183
  breakgain = m div 20,         (*minimum added space required of a break*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   184
  emergencypos = m div 2};      (*position too far to right*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   185
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   186
val margin_info = ref (make_margin_info 76);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   187
fun setmargin m = margin_info := make_margin_info m;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   188
fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   189
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   190
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   191
(* depth limitation *)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   192
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   193
val depth = ref 0;   (*maximum depth; 0 means no limit*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   194
fun setdepth dp = (depth := dp);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   195
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   196
local
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   197
  fun pruning dp (Block (m, bes, indent, wd)) =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   198
        if dp > 0
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   199
        then markup_block m (indent, map (pruning (dp - 1)) bes)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   200
        else str "..."
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   201
    | pruning dp e = e
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   202
in
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   203
  fun prune e = if ! depth > 0 then pruning (! depth) e else e;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   204
end;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   205
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   206
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   207
(* formatted output *)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   208
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   209
local
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   210
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   211
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   212
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   213
val empty: text =
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   214
 {tx = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   215
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   216
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   217
  nl = 0};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   218
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   219
fun newline {tx, ind, pos, nl} : text =
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   220
 {tx = Buffer.add (Output.output "\n") tx,
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   221
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   222
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   223
  nl = nl + 1};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   224
23628
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   225
fun control s {tx, ind, pos: int, nl} : text =
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   226
 {tx = Buffer.add s tx,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   227
  ind = ind,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   228
  pos = pos,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   229
  nl = nl};
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   230
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   231
fun string (s, len) {tx, ind, pos: int, nl} : text =
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   232
 {tx = Buffer.add s tx,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   233
  ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   234
  pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   235
  nl = nl};
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   236
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   237
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
   238
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   239
fun indentation (buf, len) {tx, ind, pos, nl} : text =
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   240
  let val s = Buffer.content buf in
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   241
   {tx = Buffer.add (mode_indent s len) tx,
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   242
    ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   243
    pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   244
    nl = nl}
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   245
  end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   246
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   247
(*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
   248
  include "after", to account for text following this block.*)
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   249
fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   250
  | 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
   251
  | breakdist (Break _ :: es, after) = 0
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   252
  | breakdist ([], after) = after;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   253
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   254
(*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
   255
fun forcenext [] = []
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   256
  | 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
   257
  | forcenext (e :: es) = e :: forcenext es;
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   258
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   259
(*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
   260
  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
   261
  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
   262
fun format ([], _, _) text = text
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   263
  | 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
   264
      (case e of
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   265
        Block (markup, bes, indent, wd) =>
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   266
          let
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   267
            val {emergencypos, ...} = ! margin_info;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   268
            val pos' = pos + indent;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   269
            val pos'' = pos' mod emergencypos;
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   270
            val block' =
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   271
              if pos' < emergencypos then (ind |> add_indent indent, pos')
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   272
              else (add_indent pos'' Buffer.empty, pos'');
23698
af84f2f13d4d moved print_mode setup for markup to markup.ML;
wenzelm
parents: 23660
diff changeset
   273
            val (bg, en) = Markup.output markup;
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   274
            val btext: text = text
23628
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   275
              |> control bg
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   276
              |> format (bes, block', breakdist (es, after))
23628
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   277
              |> control en;
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   278
            (*if this block was broken then force the next break*)
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   279
            val es' = if nl < #nl btext then forcenext es else es;
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   280
          in format (es', block, after) btext end
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   281
      | 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
   282
      | Break (force, wd) =>
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   283
          let val {margin, breakgain, ...} = ! margin_info in
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   284
            (*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
   285
              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
   286
            format (es, block, after)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   287
              (if not force andalso
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   288
                  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
   289
                then text |> blanks wd  (*just insert wd blanks*)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   290
                else text |> newline |> indentation block)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   291
          end);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   292
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   293
in
19266
2e8ad3f2cd66 added command, keyword;
wenzelm
parents: 18802
diff changeset
   294
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   295
fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   296
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   297
end;
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   298
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   299
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   300
(* special output *)
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
   301
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   302
(*symbolic markup -- no formatting*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   303
fun symbolic prt =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   304
  let
23787
4868d3913961 Buffer.markup;
wenzelm
parents: 23698
diff changeset
   305
    fun out (Block (m, [], _, _)) = Buffer.markup m I
23659
4b702ac388d6 symbolic output: avoid empty blocks, 1 space for fbreak;
wenzelm
parents: 23645
diff changeset
   306
      | out (Block (m, prts, indent, _)) =
23787
4868d3913961 Buffer.markup;
wenzelm
parents: 23698
diff changeset
   307
          Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   308
      | out (String (s, _)) = Buffer.add s
23787
4868d3913961 Buffer.markup;
wenzelm
parents: 23698
diff changeset
   309
      | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
4868d3913961 Buffer.markup;
wenzelm
parents: 23698
diff changeset
   310
      | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   311
  in out prt Buffer.empty end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   312
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   313
(*unformatted output*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   314
fun unformatted prt =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   315
  let
23787
4868d3913961 Buffer.markup;
wenzelm
parents: 23698
diff changeset
   316
    fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   317
      | fmt (String (s, _)) = Buffer.add s
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   318
      | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   319
      | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   320
  in fmt (prune prt) Buffer.empty end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   321
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   322
(*ML toplevel pretty printing*)
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   323
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
   324
  let
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   325
    fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   326
      | pp (String (s, _)) = put_str s
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   327
      | 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
   328
      | pp (Break (true, _)) = put_fbrk ()
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   329
    and pp_lst [] = ()
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   330
      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   331
  in pp (prune prt) end;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   332
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   333
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   334
(* output interfaces *)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   335
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   336
val symbolicN = "pretty_symbolic";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   337
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   338
fun output_buffer prt =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   339
  if print_mode_active symbolicN then symbolic prt
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   340
  else formatted prt;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   341
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   342
val output = Buffer.content o output_buffer;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   343
val string_of = Output.escape o output;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   344
val str_of = Output.escape o Buffer.content o unformatted;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   345
val writeln = Output.writeln o string_of;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   346
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   347
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   348
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   349
(** 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
   350
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   351
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
   352
  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
   353
14972
wenzelm
parents: 14832
diff changeset
   354
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
   355
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   356
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
   357
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   358
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
   359
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
   360
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
   361
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
   362
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
   363
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   364
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
   365
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
   366
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
   367
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
   368
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
   369
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   370
end;