src/Pure/General/pretty.ML
author wenzelm
Sun, 26 Jul 2020 21:53:29 +0200
changeset 72305 9c0b835d4cc2
parent 71678 910a081cca74
permissions -rw-r--r--
proper pretty printing for latex output, notably for pide_session=true (default);
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
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
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
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
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
69355
6bd63c94cf62 tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents: 69252
diff changeset
    26
  val make_block: {markup: Markup.output, consistent: bool, indent: int} ->
62783
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
    27
    T list -> T
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
    28
  val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    29
  val str: string -> T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    30
  val brk: int -> T
61864
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
    31
  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
    32
  val fbrk: T
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    33
  val breaks: T list -> T list
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    34
  val fbreaks: T list -> T list
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    35
  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
    36
  val block: T list -> T
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    37
  val strs: string list -> T
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    38
  val markup: Markup.T -> T list -> T
26703
c07b1a90600c removed obsolete raw_str;
wenzelm
parents: 24612
diff changeset
    39
  val mark: Markup.T -> T -> T
42266
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
    40
  val mark_str: Markup.T * string -> T
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
    41
  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
    42
  val item: T list -> T
52693
6651abced106 tuned signature;
wenzelm
parents: 51570
diff changeset
    43
  val text_fold: T list -> T
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
    44
  val keyword1: string -> T
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
    45
  val keyword2: string -> T
50162
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
    46
  val text: string -> T list
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
    47
  val paragraph: T list -> T
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
    48
  val para: string -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    49
  val quote: T -> T
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 52693
diff changeset
    50
  val cartouche: T -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    51
  val separate: string -> T list -> T list
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    52
  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
    53
  val enclose: string -> string -> T list -> T
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
    54
  val enum: string -> string -> string -> T list -> T
30620
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
    55
  val position: Position.T -> T
71678
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
    56
  val here: Position.T -> T list
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    57
  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
    58
  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
    59
  val big_list: string -> T list -> T
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
    60
  val indent: int -> T -> T
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    61
  val unbreakable: T -> T
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
    62
  val margin_default: int Unsynchronized.ref
72305
9c0b835d4cc2 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm
parents: 71678
diff changeset
    63
  val regularN: string
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    64
  val symbolicN: string
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
    65
  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
    66
  val output: int option -> T -> Output.output
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
    67
  val string_of_margin: int -> T -> string
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
    68
  val string_of: T -> string
49656
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
    69
  val writeln: T -> unit
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
    70
  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
    71
  val symbolic_string_of: T -> string
61879
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61872
diff changeset
    72
  val unformatted_string_of: T -> string
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    73
  val markup_chunks: Markup.T -> T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    74
  val chunks: T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    75
  val chunks2: T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    76
  val block_enclose: T * T -> T list -> T
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    77
  val writeln_chunks: T list -> unit
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
    78
  val writeln_chunks2: T list -> unit
62784
0371c369ab1d adapted to Poly/ML repository version 2e40cadc975a;
wenzelm
parents: 62783
diff changeset
    79
  val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
36748
wenzelm
parents: 36747
diff changeset
    80
  val from_ML: ML_Pretty.pretty -> T
68919
3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents: 67522
diff changeset
    81
  val to_polyml: T -> PolyML.pretty
3a0db30e5d87 simplified signature (again, see 751bcf0473a7): e.g. relevant for non-Isabelle ML environments;
wenzelm
parents: 67522
diff changeset
    82
  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
    83
end;
6116
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
structure Pretty: PRETTY =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    86
struct
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
    87
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    88
(** print mode operations **)
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    89
61867
6dcc9e4f1aa6 tuned signature;
wenzelm
parents: 61866
diff changeset
    90
fun default_indent (_: string) = Symbol.spaces;
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    91
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    92
local
23698
af84f2f13d4d moved print_mode setup for markup to markup.ML;
wenzelm
parents: 23660
diff changeset
    93
  val default = {indent = default_indent};
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
    94
  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
    95
in
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
    96
  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
    97
    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
    98
      (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
    99
       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
   100
       Symtab.update (name, {indent = indent}) tab));
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   101
  fun get_mode () =
43684
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
   102
    the_default default
85388f5570c4 prefer Synchronized.var;
wenzelm
parents: 42383
diff changeset
   103
      (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
   104
end;
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   105
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   106
fun mode_indent x y = #indent (get_mode ()) x y;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   107
61867
6dcc9e4f1aa6 tuned signature;
wenzelm
parents: 61866
diff changeset
   108
val output_spaces = Output.output o Symbol.spaces;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   109
val add_indent = Buffer.add o output_spaces;
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   110
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   111
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   112
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   113
(** printing items: compound phrases, strings, and breaks **)
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   114
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   115
val force_nat = Integer.max 0;
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   116
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   117
abstype T =
69355
6bd63c94cf62 tuned signature (see also src/Tools/Haskell/Markup.hs);
wenzelm
parents: 69252
diff changeset
   118
    Block of Markup.output * bool * int * T list * int
61871
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61867
diff changeset
   119
      (*markup output, consistent, indentation, body, length*)
61864
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   120
  | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
61872
wenzelm
parents: 61871
diff changeset
   121
  | Str of Output.output * int  (*text, length*)
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   122
with
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   123
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   124
fun length (Block (_, _, _, _, len)) = len
61872
wenzelm
parents: 61871
diff changeset
   125
  | length (Break (_, wd, _)) = wd
wenzelm
parents: 61871
diff changeset
   126
  | length (Str (_, len)) = len;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   127
62783
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   128
fun make_block {markup, consistent, indent} body =
61885
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   129
  let
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   130
    val indent' = force_nat indent;
61885
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   131
    fun body_length prts len =
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   132
      let
67522
9e712280cc37 clarified take/drop/chop prefix/suffix;
wenzelm
parents: 62899
diff changeset
   133
        val (line, rest) = chop_prefix (fn Break (true, _, _) => false | _ => true) prts;
61885
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   134
        val len' = Int.max (fold (Integer.add o length) line 0, len);
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   135
      in
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   136
        (case rest of
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   137
          Break (true, _, ind) :: rest' =>
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   138
            body_length (Break (false, indent' + ind, 0) :: rest') len'
61885
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   139
        | [] => len')
c0f34fe6aa61 clarified length of block with pre-existant forced breaks;
wenzelm
parents: 61879
diff changeset
   140
      end;
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   141
  in Block (markup, consistent, indent', body, body_length body 0) end;
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   142
62783
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   143
fun markup_block {markup, consistent, indent} es =
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   144
  make_block {markup = Markup.output markup, consistent = consistent, indent = indent} es;
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   145
9730
11d137b25555 added indent;
wenzelm
parents: 9121
diff changeset
   146
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   147
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   148
(** derived operations to create formatting expressions **)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   149
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   150
val str = Output.output_width ##> force_nat #> Str;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   151
62785
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   152
fun brk wd = Break (false, force_nat wd, 0);
70b9c7d4ed7f more robust pretty printing: permissive treatment of bad values;
wenzelm
parents: 62784
diff changeset
   153
fun brk_indent wd ind = Break (false, force_nat wd, ind);
61864
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   154
val fbrk = Break (true, 1, 0);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   155
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   156
fun breaks prts = Library.separate (brk 1) prts;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   157
fun fbreaks prts = Library.separate fbrk prts;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   158
62783
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   159
fun blk (indent, es) =
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   160
  markup_block {markup = Markup.empty, consistent = false, indent = indent} es;
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   161
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   162
fun block prts = blk (2, prts);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   163
val strs = block o breaks o map str;
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   164
62783
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   165
fun markup m = markup_block {markup = m, consistent = false, indent = 0};
42266
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   166
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   167
fun mark_str (m, s) = mark m (str s);
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   168
fun marks_str (ms, s) = fold_rev mark ms (str s);
f87e0be80a3f clarified Pretty.mark;
wenzelm
parents: 40131
diff changeset
   169
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
   170
val item = markup Markup.item;
52693
6651abced106 tuned signature;
wenzelm
parents: 51570
diff changeset
   171
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
   172
55763
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
   173
fun keyword1 name = mark_str (Markup.keyword1, name);
4b3907cb5654 tuned signature;
wenzelm
parents: 55033
diff changeset
   174
fun keyword2 name = mark_str (Markup.keyword2, name);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   175
50162
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
   176
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
   177
val paragraph = markup Markup.paragraph;
50162
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
   178
val para = paragraph o text;
e06eabc421e7 some support for breakable text and paragraphs;
wenzelm
parents: 49656
diff changeset
   179
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   180
fun quote prt = blk (1, [str "\"", prt, str "\""]);
62210
e068ea693678 tuned signature (according to Scala version);
wenzelm
parents: 62094
diff changeset
   181
fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   182
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   183
fun separate sep prts =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   184
  flat (Library.separate [str sep, brk 1] (map single prts));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   185
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   186
val commas = separate ",";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   187
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   188
fun enclose lpar rpar prts =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   189
  block (str lpar :: (prts @ [str rpar]));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   190
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   191
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
   192
30620
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   193
val position =
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   194
  enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   195
71678
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   196
fun here pos =
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   197
  let
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   198
    val props = Position.properties_of pos;
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   199
    val (s1, s2) = Position.here_strs pos;
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   200
  in
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   201
    if s2 = "" then []
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   202
    else [str s1, mark_str (Markup.properties props Markup.position, s2)]
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   203
  end;
910a081cca74 more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents: 69355
diff changeset
   204
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   205
val list = enum ",";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   206
fun str_list lpar rpar strs = list lpar rpar (map str strs);
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   207
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   208
fun big_list name prts = block (fbreaks (str name :: prts));
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   209
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   210
fun indent 0 prt = prt
61867
6dcc9e4f1aa6 tuned signature;
wenzelm
parents: 61866
diff changeset
   211
  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   212
61872
wenzelm
parents: 61871
diff changeset
   213
fun unbreakable (Block (m, consistent, indent, es, len)) =
61871
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61867
diff changeset
   214
      Block (m, consistent, indent, map unbreakable es, len)
61872
wenzelm
parents: 61871
diff changeset
   215
  | unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd)
wenzelm
parents: 61871
diff changeset
   216
  | unbreakable (e as Str _) = e;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   217
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   218
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   219
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   220
(** formatting **)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   221
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   222
(* formatted output *)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   223
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   224
local
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   225
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   226
type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   227
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   228
val empty: text =
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   229
 {tx = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   230
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   231
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   232
  nl = 0};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   233
32784
1a5dde5079ac eliminated redundant bindings;
wenzelm
parents: 32738
diff changeset
   234
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
   235
 {tx = Buffer.add (Output.output "\n") tx,
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   236
  ind = Buffer.empty,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   237
  pos = 0,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   238
  nl = nl + 1};
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   239
23628
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   240
fun control s {tx, ind, pos: int, nl} : text =
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   241
 {tx = Buffer.add s tx,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   242
  ind = ind,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   243
  pos = pos,
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   244
  nl = nl};
41cdbfb9f77b markup: emit as control information -- no indent text;
wenzelm
parents: 23617
diff changeset
   245
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   246
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
   247
 {tx = Buffer.add s tx,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   248
  ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   249
  pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   250
  nl = nl};
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   251
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   252
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
   253
17756
d4a35f82fbb4 minor tweaks for Poplog/ML;
wenzelm
parents: 17542
diff changeset
   254
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
   255
  let val s = Buffer.content buf in
23617
840904fc1eb1 added print_mode setup: indent and markup;
wenzelm
parents: 22019
diff changeset
   256
   {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
   257
    ind = Buffer.add s ind,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   258
    pos = pos + len,
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   259
    nl = nl}
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   260
  end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   261
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   262
(*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
   263
  include "after", to account for text following this block.*)
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   264
fun break_dist (Break _ :: _, _) = 0
61872
wenzelm
parents: 61871
diff changeset
   265
  | break_dist (e :: es, after) = length e + break_dist (es, after)
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   266
  | break_dist ([], after) = after;
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   267
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   268
val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   269
val force_all = map force_break;
10952
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   270
b520e4f1313b support general indentation (e.g. for non-tt latex output);
wenzelm
parents: 9730
diff changeset
   271
(*Search for the next break (at this or higher levels) and force it to occur.*)
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   272
fun force_next [] = []
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   273
  | force_next ((e as Break _) :: es) = force_break e :: es
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   274
  | 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
   275
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   276
in
19266
2e8ad3f2cd66 added command, keyword;
wenzelm
parents: 18802
diff changeset
   277
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   278
fun formatted margin input =
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   279
  let
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   280
    val breakgain = margin div 20;     (*minimum added space required of a break*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   281
    val emergencypos = margin div 2;   (*position too far to right*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   282
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   283
    (*es is list of expressions to print;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   284
      blockin is the indentation of the current block;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   285
      after is the width of the following context until next break.*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   286
    fun format ([], _, _) text = text
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   287
      | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   288
          (case e of
61871
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61867
diff changeset
   289
            Block ((bg, en), consistent, indent, bes, blen) =>
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   290
              let
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   291
                val pos' = pos + indent;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   292
                val pos'' = pos' mod emergencypos;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   293
                val block' =
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   294
                  if pos' < emergencypos then (ind |> add_indent indent, pos')
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   295
                  else (add_indent pos'' Buffer.empty, pos'');
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   296
                val d = break_dist (es, after)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   297
                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
   298
                val btext: text = text
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   299
                  |> control bg
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   300
                  |> format (bes', block', d)
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   301
                  |> control en;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   302
                (*if this block was broken then force the next break*)
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   303
                val es' = if nl < #nl btext then force_next es else es;
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   304
              in format (es', block, after) btext end
61864
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   305
          | Break (force, wd, ind) =>
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   306
              (*no break if text to next break fits on this line
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   307
                or if breaking would add only breakgain to space*)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   308
              format (es, block, after)
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   309
                (if not force andalso
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   310
                    pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   311
                 then text |> blanks wd  (*just insert wd blanks*)
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   312
                 else text |> newline |> indentation block |> blanks ind)
61872
wenzelm
parents: 61871
diff changeset
   313
          | Str str => format (es, block, after) (string str text));
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   314
  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
   315
    #tx (format ([input], (Buffer.empty, 0), 0) empty)
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   316
  end;
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   317
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   318
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
   319
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   320
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   321
(* special output *)
18802
f449d516f36b renamed gen_list to enum;
wenzelm
parents: 18603
diff changeset
   322
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   323
(*symbolic markup -- no formatting*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   324
fun symbolic prt =
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   325
  let
61871
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61867
diff changeset
   326
    fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61867
diff changeset
   327
      | out (Block ((bg, en), consistent, indent, prts, _)) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43684
diff changeset
   328
          Buffer.add bg #>
61866
3a5992c3410c support for blocks with consistent breaks;
wenzelm
parents: 61865
diff changeset
   329
          Buffer.markup (Markup.block consistent indent) (fold out prts) #>
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 43684
diff changeset
   330
          Buffer.add en
61864
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   331
      | out (Break (false, wd, ind)) =
e2a9e46ac0fb support pretty break indent, like underlying ML systems;
wenzelm
parents: 56334
diff changeset
   332
          Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
61872
wenzelm
parents: 61871
diff changeset
   333
      | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
wenzelm
parents: 61871
diff changeset
   334
      | out (Str (s, _)) = Buffer.add s;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   335
  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
   336
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   337
(*unformatted output*)
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   338
fun unformatted prt =
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   339
  let
69252
wenzelm
parents: 68919
diff changeset
   340
    fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
wenzelm
parents: 68919
diff changeset
   341
      | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
wenzelm
parents: 68919
diff changeset
   342
      | out (Str (s, _)) = Buffer.add s;
wenzelm
parents: 68919
diff changeset
   343
  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
   344
30624
e755b8b76365 simplified datatype ML_Pretty.pretty: model Isabelle not Poly/ML;
wenzelm
parents: 30620
diff changeset
   345
36748
wenzelm
parents: 36747
diff changeset
   346
(* output interfaces *)
30620
16b7ecc183e5 added position;
wenzelm
parents: 29606
diff changeset
   347
62899
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   348
val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   349
72305
9c0b835d4cc2 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm
parents: 71678
diff changeset
   350
val regularN = "pretty_regular";
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   351
val symbolicN = "pretty_symbolic";
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   352
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   353
fun output_buffer margin prt =
72305
9c0b835d4cc2 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm
parents: 71678
diff changeset
   354
  if print_mode_active symbolicN andalso not (print_mode_active regularN)
9c0b835d4cc2 proper pretty printing for latex output, notably for pide_session=true (default);
wenzelm
parents: 71678
diff changeset
   355
  then symbolic prt
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   356
  else formatted (the_default (! margin_default) margin) prt;
23645
d220d12bd45e export mode_markup;
wenzelm
parents: 23638
diff changeset
   357
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   358
val output = Buffer.content oo output_buffer;
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   359
fun string_of_margin margin = Output.escape o output (SOME margin);
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 36733
diff changeset
   360
val string_of = Output.escape o output NONE;
49656
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   361
val writeln = Output.writeln o string_of;
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   362
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   363
val symbolic_output = Buffer.content o symbolic;
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   364
val symbolic_string_of = Output.escape o symbolic_output;
7ff712de5747 treat wrapped markup elements as raw markup delimiters;
wenzelm
parents: 49565
diff changeset
   365
61879
276ad4354069 renamed Pretty.str_of to Pretty.unformatted_string_of to emphasize its meaning;
wenzelm
parents: 61872
diff changeset
   366
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
   367
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   368
56334
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   369
(* chunks *)
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   370
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   371
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
   372
val chunks = markup_chunks Markup.empty;
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   373
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   374
fun chunks2 prts =
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   375
  (case try split_last prts of
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   376
    NONE => blk (0, [])
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   377
  | SOME (prefix, last) =>
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   378
      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
   379
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   380
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
   381
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   382
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
   383
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   384
fun writeln_chunks prts =
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   385
  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
   386
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   387
fun writeln_chunks2 prts =
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   388
  (case try split_last prts of
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   389
    NONE => ()
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   390
  | SOME (prefix, last) =>
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   391
      (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
   392
        [string_of_text_fold last])
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   393
      |> Output.writelns);
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   394
6b3739fee456 some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents: 55918
diff changeset
   395
14832
6589a58f57cb pp: abstract pretty printing context; string_of/str_of: mark result as raw output; added Pretty.unbreakable;
wenzelm
parents: 12421
diff changeset
   396
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62389
diff changeset
   397
(** toplevel pretty printing **)
36748
wenzelm
parents: 36747
diff changeset
   398
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   399
fun to_ML 0 (Block _) = ML_Pretty.str "..."
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   400
  | to_ML depth (Block (m, consistent, indent, prts, _)) =
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   401
      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
   402
  | to_ML _ (Break (force, wd, ind)) =
62389
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   403
      ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   404
  | to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
36748
wenzelm
parents: 36747
diff changeset
   405
61871
ba466ac335e3 clarified underlying datatypes;
wenzelm
parents: 61867
diff changeset
   406
fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
62783
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   407
      make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent}
75ee05386b90 explicit mixfix block properties;
wenzelm
parents: 62672
diff changeset
   408
        (map from_ML prts)
62389
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   409
  | from_ML (ML_Pretty.Break (force, wd, ind)) =
ad3eb2889f9a support for polyml-git ec49a49972c5 (branch FixedPrecisionInt);
wenzelm
parents: 62210
diff changeset
   410
      Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
62820
5c678ee5d34a proper type;
wenzelm
parents: 62819
diff changeset
   411
  | from_ML (ML_Pretty.String (s, len)) = Str (s, force_nat (FixedInt.toInt len));
36748
wenzelm
parents: 36747
diff changeset
   412
62667
254582abf067 clarified Pretty.T toplevel pp;
wenzelm
parents: 62663
diff changeset
   413
val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62389
diff changeset
   414
val from_polyml = ML_Pretty.from_polyml #> from_ML;
bea354f6ff21 clarified modules;
wenzelm
parents: 62389
diff changeset
   415
37529
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   416
end;
a23e8aa853eb treat Pretty.T as strictly abstract type;
wenzelm
parents: 37193
diff changeset
   417
62819
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62785
diff changeset
   418
val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62785
diff changeset
   419
val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 62389
diff changeset
   420
6116
8ba2f25610f7 files scan.ML, source.ML, symbol.ML, pretty.ML moved to Pure/General;
wenzelm
parents:
diff changeset
   421
end;
62899
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   422
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   423
structure ML_Pretty =
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   424
struct
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   425
  open ML_Pretty;
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   426
  val string_of_polyml = Pretty.string_of o Pretty.from_polyml;
845ed4584e21 clarified bootstrap of @{make_string} -- avoid query on ML environment;
wenzelm
parents: 62823
diff changeset
   427
end;