| changeset 80855 | 301612847ea3 |
| parent 80846 | 9ed32b8a03a9 |
| child 80862 | ab0234b9af65 |
--- a/src/Pure/General/latex.ML Wed Sep 11 17:00:02 2024 +0200 +++ b/src/Pure/General/latex.ML Wed Sep 11 19:35:21 2024 +0200 @@ -270,7 +270,8 @@ in fun output_ops opt_margin : Pretty.output_ops = - {output = output_width, + {symbolic = false, + output = output_width, markup = latex_markup_output, indent = latex_indent, margin = ML_Pretty.get_margin opt_margin};