changeset 74779 | 5fca489a6ac1 |
parent 73780 | 466fae6bf22e |
child 74780 | 6504e9b09926 |
--- a/src/Pure/Thy/latex.ML Sat Nov 13 17:22:10 2021 +0100 +++ b/src/Pure/Thy/latex.ML Sat Nov 13 17:26:35 2021 +0100 @@ -46,8 +46,10 @@ type text = XML.body; -fun text ("", _) = [] - | text (s, pos) = [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])]; +fun text (s, pos) = + if s = "" then [] + else if pos = Position.none then [XML.Text s] + else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])]; fun string s = text (s, Position.none);