88 * Constructors for type Pretty.T (such as Pretty.str, Pretty.mark_str, |
88 * Constructors for type Pretty.T (such as Pretty.str, Pretty.mark_str, |
89 Pretty.markup_block) are now value-oriented. Use of the global |
89 Pretty.markup_block) are now value-oriented. Use of the global |
90 print_mode is restricted to ultimate Pretty.string_of (and some |
90 print_mode is restricted to ultimate Pretty.string_of (and some |
91 variants), while the underlying Pretty.output operation supports an |
91 variants), while the underlying Pretty.output operation supports an |
92 explicit Pretty.output_ops argument for alternative applications. |
92 explicit Pretty.output_ops argument for alternative applications. |
|
93 |
|
94 * The print_mode "latex" only affects inner syntax variants, while its |
|
95 impact on Output/Markup/Pretty operations has been removed. Instead, |
|
96 there are explicit operations Latex.output_, Latex.escape, and |
|
97 Latex.output_ops. Output.output has been renamed to Output.output_ to |
|
98 indicate statically where Isabelle/ML implementations may have to be |
|
99 changed. Rare INCOMPATIBILITY for ambitious document antiquotations that |
|
100 generate LaTeX source on their own account, instead of using regular |
|
101 Pretty.T interfaces. The following operations need to be adjusted as |
|
102 follows: |
|
103 |
|
104 Output.output |
|
105 becomes Output.output_ or Latex.output_ |
|
106 Output.escape |
|
107 is omitted or becomes Latex.escape |
|
108 Pretty.string_of with implicit "latex" print_mode |
|
109 becomes Pretty.string_of_ops with explicit Latex.output_ops |
|
110 |
|
111 Note that basic Markup.markup cannot be used for Latex output: proper |
|
112 Pretty.T operations are required (e.g. Pretty.mark_str). |
93 |
113 |
94 |
114 |
95 *** System *** |
115 *** System *** |
96 |
116 |
97 * The Build_Manager module has replaced previous glue-code for Jenkins |
117 * The Build_Manager module has replaced previous glue-code for Jenkins |