src/Pure/General/pretty.ML
author wenzelm
Fri, 18 Mar 2016 21:21:09 +0100
changeset 62672 068b430e678f
parent 62667 254582abf067
child 62783 75ee05386b90
permissions -rw-r--r--
clarified print depth;
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
8806
wenzelm
parents: 8456
diff changeset
     2
    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
     3
    Author:     Markus Wenzel, TU Munich
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     4
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     5
Generic pretty printing module.
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     6
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     7
Loosely based on
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     8
  D. C. Oppen, "Pretty Printing",
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
     9
  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
    10
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    11
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
    12
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
    13
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
    14
text is indented to the level of the enclosing block.  Normally, if a block
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
    15
is broken then all enclosing blocks will also be broken.
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    16
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
    17
The stored length of a block is used in break_dist (to treat each inner block as
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    18
a unit for breaking).
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    19
*)
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    20
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    21
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
    22
sig
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 38474
diff changeset
    23
  val default_indent: string -> int -> Output.output
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 38474
diff changeset
    24
  val add_mode: string -> (string -> int -> Output.output) -> unit
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    25
  type T
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
    26
  val make_block: Output.output * Output.output -> bool -> int -> T list -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    27
  val str: string -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    28
  val brk: int -> T
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
    29
  val brk_indent: int -> int -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    30
  val fbrk: T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    31
  val breaks: T list -> T list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    32
  val fbreaks: T list -> T list
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    33
  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
    34
  val block: T list -> T
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    35
  val strs: string list -> T
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    36
  val markup: Markup.T -> T list -> T
26703
c07b1a90600c removed obsolete raw_str;
wenzelm
parents: 24612
diff changeset
    37
  val mark: Markup.T -> T -> T
42266
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
    38
  val mark_str: Markup.T * string -> T
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
    39
  val marks_str: Markup.T list * string -> T
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 51511
diff changeset
    40
  val item: T list -> T
52693
6651abced106 tuned signature;
wenzelm
parents: 51570
diff changeset
    41
  val text_fold: T list -> T
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
    42
  val keyword1: string -> T
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
    43
  val keyword2: string -> T
50162
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
    44
  val text: string -> T list
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
    45
  val paragraph: T list -> T
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
    46
  val para: string -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    47
  val quote: T -> T
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 52693
diff changeset
    48
  val cartouche: T -> T
18802
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
30620
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
    53
  val position: Position.T -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    54
  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
    55
  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
    56
  val big_list: string -> T list -> T
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
    57
  val indent: int -> T -> T
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    58
  val unbreakable: T -> T
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
    59
  val margin_default: int Unsynchronized.ref
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    60
  val symbolicN: string
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
    61
  val output_buffer: int option -> T -> Buffer.T
40131
7cbebd636e79 explicitly qualify type Output.output, which is a slightly odd internal feature;
wenzelm
parents: 38474
diff changeset
    62
  val output: int option -> T -> Output.output
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
    63
  val string_of_margin: int -> T -> string
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    64
  val string_of: T -> string
49656
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
    65
  val writeln: T -> unit
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
    66
  val symbolic_output: T -> Output.output
49565
ea4308b7ef0f ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents: 49554
diff changeset
    67
  val symbolic_string_of: T -> string
61877
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61870
diff changeset
    68
  val unformatted_string_of: T -> string
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    69
  val markup_chunks: Markup.T -> T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    70
  val chunks: T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    71
  val chunks2: T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    72
  val block_enclose: T * T -> T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    73
  val writeln_chunks: T list -> unit
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    74
  val writeln_chunks2: T list -> unit
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
    75
  val to_ML: int -> T -> ML_Pretty.pretty
36748
wenzelm
parents: 36747
diff changeset
    76
  val from_ML: ML_Pretty.pretty -> T
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
    77
  val to_polyml: T -> PolyML.pretty
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
    78
  val from_polyml: PolyML.pretty -> 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
    79
end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    80
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    81
structure Pretty: PRETTY =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    82
struct
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    83
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    84
(** print mode operations **)
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    85
61865
6dcc9e4f1aa6 tuned signature;
wenzelm
parents: 61864
diff changeset
    86
fun default_indent (_: string) = Symbol.spaces;
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    87
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    88
local
23698
af84f2f13d4d moved print_mode setup for markup to markup.ML;
wenzelm
parents: 23660
diff changeset
    89
  val default = {indent = default_indent};
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
    90
  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    91
in
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
    92
  fun add_mode name indent =
46894
e2ad717ec889 allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents: 45666
diff changeset
    93
    Synchronized.change modes (fn tab =>
e2ad717ec889 allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents: 45666
diff changeset
    94
      (if not (Symtab.defined tab name) then ()
e2ad717ec889 allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents: 45666
diff changeset
    95
       else warning ("Redefining pretty mode " ^ quote name);
e2ad717ec889 allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;
wenzelm
parents: 45666
diff changeset
    96
       Symtab.update (name, {indent = indent}) tab));
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    97
  fun get_mode () =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
    98
    the_default default
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
    99
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   100
end;
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   101
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   102
fun mode_indent x y = #indent (get_mode ()) x y;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   103
61865
6dcc9e4f1aa6 tuned signature;
wenzelm
parents: 61864
diff changeset
   104
val output_spaces = Output.output o Symbol.spaces;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   105
val add_indent = Buffer.add o output_spaces;
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   106
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   107
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   108
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   109
(** printing items: compound phrases, strings, and breaks **)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   110
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   111
abstype T =
61869
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   112
    Block of (Output.output * Output.output) * bool * int * T list * int
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   113
      (*markup output, consistent, indentation, body, length*)
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   114
  | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
61870
wenzelm
parents: 61869
diff changeset
   115
  | Str of Output.output * int  (*text, length*)
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   116
with
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   117
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   118
fun length (Block (_, _, _, _, len)) = len
61870
wenzelm
parents: 61869
diff changeset
   119
  | length (Break (_, wd, _)) = wd
wenzelm
parents: 61869
diff changeset
   120
  | length (Str (_, len)) = len;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   121
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   122
fun make_block markup consistent indent body =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   123
  let
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   124
    fun body_length prts len =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   125
      let
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   126
        val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   127
        val len' = Int.max (fold (Integer.add o length) line 0, len);
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   128
      in
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   129
        (case rest of
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   130
          Break (true, _, ind) :: rest' =>
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   131
            body_length (Break (false, indent + ind, 0) :: rest') len'
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   132
        | [] => len')
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   133
      end;
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   134
  in Block (markup, consistent, indent, body, body_length body 0) end;
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   135
61883
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   136
fun markup_block markup indent es =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61877
diff changeset
   137
  make_block (Markup.output markup) false indent es;
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   138
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
   139
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   140
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   141
(** derived operations to create formatting expressions **)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   142
61870
wenzelm
parents: 61869
diff changeset
   143
val str = Str o Output.output_width;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   144
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   145
fun brk wd = Break (false, wd, 0);
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   146
fun brk_indent wd ind = Break (false, wd, ind);
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   147
val fbrk = Break (true, 1, 0);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   148
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   149
fun breaks prts = Library.separate (brk 1) prts;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   150
fun fbreaks prts = Library.separate fbrk prts;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   151
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   152
fun blk (ind, es) = markup_block Markup.empty ind es;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   153
fun block prts = blk (2, prts);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   154
val strs = block o breaks o map str;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   155
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   156
fun markup m = markup_block m 0;
42266
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   157
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   158
fun mark_str (m, s) = mark m (str s);
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   159
fun marks_str (ms, s) = fold_rev mark ms (str s);
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   160
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 51511
diff changeset
   161
val item = markup Markup.item;
52693
6651abced106 tuned signature;
wenzelm
parents: 51570
diff changeset
   162
val text_fold = markup Markup.text_fold;
51570
3633828d80fc basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents: 51511
diff changeset
   163
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
   164
fun keyword1 name = mark_str (Markup.keyword1, name);
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
   165
fun keyword2 name = mark_str (Markup.keyword2, name);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   166
50162
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
   167
val text = breaks o map str o Symbol.explode_words;
50201
c26369c9eda6 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents: 50162
diff changeset
   168
val paragraph = markup Markup.paragraph;
50162
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
   169
val para = paragraph o text;
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
   170
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   171
fun quote prt = blk (1, [str "\"", prt, str "\""]);
62210
e068ea693678 tuned signature (according to Scala version);
wenzelm
parents: 62094
diff changeset
   172
fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   173
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   174
fun separate sep prts =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   175
  flat (Library.separate [str sep, brk 1] (map single prts));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   176
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   177
val commas = separate ",";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   178
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   179
fun enclose lpar rpar prts =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   180
  block (str lpar :: (prts @ [str rpar]));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   181
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   182
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
   183
30620
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   184
val position =
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   185
  enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   186
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   187
val list = enum ",";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   188
fun str_list lpar rpar strs = list lpar rpar (map str strs);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   189
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   190
fun big_list name prts = block (fbreaks (str name :: prts));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   191
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   192
fun indent 0 prt = prt
61865
6dcc9e4f1aa6 tuned signature;
wenzelm
parents: 61864
diff changeset
   193
  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   194
61870
wenzelm
parents: 61869
diff changeset
   195
fun unbreakable (Block (m, consistent, indent, es, len)) =
61869
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   196
      Block (m, consistent, indent, map unbreakable es, len)
61870
wenzelm
parents: 61869
diff changeset
   197
  | unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd)
wenzelm
parents: 61869
diff changeset
   198
  | unbreakable (e as Str _) = e;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   199
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   200
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   201
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   202
(** formatting **)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   203
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   204
(* formatted output *)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   205
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   206
local
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   207
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   208
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   209
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   210
val empty: text =
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   211
 {tx = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   212
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   213
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   214
  nl = 0};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   215
32784
1a5dde5079ac eliminated redundant bindings;
wenzelm
parents: 32738
diff changeset
   216
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
   217
 {tx = Buffer.add (Output.output "\n") tx,
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   218
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   219
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   220
  nl = nl + 1};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   221
23628
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   222
fun control s {tx, ind, pos: int, nl} : text =
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   223
 {tx = Buffer.add s tx,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   224
  ind = ind,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   225
  pos = pos,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   226
  nl = nl};
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   227
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   228
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
   229
 {tx = Buffer.add s tx,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   230
  ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   231
  pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   232
  nl = nl};
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   233
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   234
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
   235
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   236
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
   237
  let val s = Buffer.content buf in
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   238
   {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
   239
    ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   240
    pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   241
    nl = nl}
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   242
  end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   243
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   244
(*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
   245
  include "after", to account for text following this block.*)
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   246
fun break_dist (Break _ :: _, _) = 0
61870
wenzelm
parents: 61869
diff changeset
   247
  | break_dist (e :: es, after) = length e + break_dist (es, after)
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   248
  | break_dist ([], after) = after;
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   249
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   250
val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   251
val force_all = map force_break;
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   252
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   253
(*Search for the next break (at this or higher levels) and force it to occur.*)
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   254
fun force_next [] = []
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   255
  | force_next ((e as Break _) :: es) = force_break e :: es
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   256
  | force_next (e :: es) = e :: force_next es;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   257
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   258
in
19266
2e8ad3f2cd66 added command, keyword;
wenzelm
parents: 18802
diff changeset
   259
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   260
fun formatted margin input =
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   261
  let
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   262
    val breakgain = margin div 20;     (*minimum added space required of a break*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   263
    val emergencypos = margin div 2;   (*position too far to right*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   264
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   265
    (*es is list of expressions to print;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   266
      blockin is the indentation of the current block;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   267
      after is the width of the following context until next break.*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   268
    fun format ([], _, _) text = text
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   269
      | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   270
          (case e of
61869
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   271
            Block ((bg, en), consistent, indent, bes, blen) =>
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   272
              let
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   273
                val pos' = pos + indent;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   274
                val pos'' = pos' mod emergencypos;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   275
                val block' =
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   276
                  if pos' < emergencypos then (ind |> add_indent indent, pos')
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   277
                  else (add_indent pos'' Buffer.empty, pos'');
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   278
                val d = break_dist (es, after)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   279
                val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   280
                val btext: text = text
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   281
                  |> control bg
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   282
                  |> format (bes', block', d)
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   283
                  |> control en;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   284
                (*if this block was broken then force the next break*)
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   285
                val es' = if nl < #nl btext then force_next es else es;
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   286
              in format (es', block, after) btext end
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   287
          | Break (force, wd, ind) =>
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   288
              (*no break if text to next break fits on this line
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   289
                or if breaking would add only breakgain to space*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   290
              format (es, block, after)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   291
                (if not force andalso
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   292
                    pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   293
                 then text |> blanks wd  (*just insert wd blanks*)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   294
                 else text |> newline |> indentation block |> blanks ind)
61870
wenzelm
parents: 61869
diff changeset
   295
          | Str str => format (es, block, after) (string str text));
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   296
  in
36747
7361d5dde9ce discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
wenzelm
parents: 36745
diff changeset
   297
    #tx (format ([input], (Buffer.empty, 0), 0) empty)
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   298
  end;
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
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
   301
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   302
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   303
(* special output *)
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
   304
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   305
(*symbolic markup -- no formatting*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   306
fun symbolic prt =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   307
  let
61869
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   308
    fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   309
      | out (Block ((bg, en), consistent, indent, prts, _)) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43684
diff changeset
   310
          Buffer.add bg #>
61864
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61863
diff changeset
   311
          Buffer.markup (Markup.block consistent indent) (fold out prts) #>
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43684
diff changeset
   312
          Buffer.add en
61862
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   313
      | out (Break (false, wd, ind)) =
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   314
          Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
61870
wenzelm
parents: 61869
diff changeset
   315
      | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
wenzelm
parents: 61869
diff changeset
   316
      | out (Str (s, _)) = Buffer.add s;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   317
  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
   318
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   319
(*unformatted output*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   320
fun unformatted prt =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   321
  let
61869
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   322
    fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
61870
wenzelm
parents: 61869
diff changeset
   323
      | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd)
wenzelm
parents: 61869
diff changeset
   324
      | fmt (Str (s, _)) = Buffer.add s;
36747
7361d5dde9ce discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;
wenzelm
parents: 36745
diff changeset
   325
  in fmt prt Buffer.empty end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   326
30624
e755b8b76365 simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents: 30620
diff changeset
   327
36748
wenzelm
parents: 36747
diff changeset
   328
(* output interfaces *)
30620
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   329
36748
wenzelm
parents: 36747
diff changeset
   330
val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   331
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   332
val symbolicN = "pretty_symbolic";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   333
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   334
fun output_buffer margin prt =
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   335
  if print_mode_active symbolicN then symbolic prt
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   336
  else formatted (the_default (! margin_default) margin) prt;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   337
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   338
val output = Buffer.content oo output_buffer;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   339
fun string_of_margin margin = Output.escape o output (SOME margin);
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   340
val string_of = Output.escape o output NONE;
49656
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   341
val writeln = Output.writeln o string_of;
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   342
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   343
val symbolic_output = Buffer.content o symbolic;
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   344
val symbolic_string_of = Output.escape o symbolic_output;
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   345
61877
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61870
diff changeset
   346
val unformatted_string_of = Output.escape o Buffer.content o unformatted;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   347
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   348
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   349
(* chunks *)
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   350
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   351
fun markup_chunks m prts = markup m (fbreaks (map (text_fold o single) prts));
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   352
val chunks = markup_chunks Markup.empty;
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   353
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   354
fun chunks2 prts =
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   355
  (case try split_last prts of
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   356
    NONE => blk (0, [])
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   357
  | SOME (prefix, last) =>
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   358
      blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   359
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   360
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   361
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   362
fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   363
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   364
fun writeln_chunks prts =
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   365
  Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   366
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   367
fun writeln_chunks2 prts =
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   368
  (case try split_last prts of
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   369
    NONE => ()
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   370
  | SOME (prefix, last) =>
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   371
      (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   372
        [string_of_text_fold last])
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   373
      |> Output.writelns);
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   374
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   375
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   376
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
   377
(** toplevel pretty printing **)
36748
wenzelm
parents: 36747
diff changeset
   378
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   379
fun to_ML 0 (Block _) = ML_Pretty.str "..."
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   380
  | to_ML depth (Block (m, consistent, indent, prts, _)) =
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   381
      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map (to_ML (depth - 1)) prts)
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   382
  | to_ML _ (Break (force, wd, ind)) =
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   383
      ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   384
  | to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
36748
wenzelm
parents: 36747
diff changeset
   385
61869
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61865
diff changeset
   386
fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
62387
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   387
      make_block m consistent (FixedInt.toInt indent) (map from_ML prts)
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   388
  | from_ML (ML_Pretty.Break (force, wd, ind)) =
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   389
      Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   390
  | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
36748
wenzelm
parents: 36747
diff changeset
   391
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   392
val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
   393
val from_polyml = ML_Pretty.from_polyml #> from_ML;
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
   394
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   395
end;
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   396
62672
068b430e678f clarified print depth;
wenzelm
parents: 62667
diff changeset
   397
val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
   398
val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
bea354f6ff21 clarified modules;
wenzelm
parents: 62387
diff changeset
   399
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   400
end;