diff -r a1a316442a9b -r 5fca489a6ac1 src/Pure/Thy/latex.ML --- 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);