# HG changeset patch
# User wenzelm
# Date 1636820795 -3600
# Node ID 5fca489a6ac1f5795ce424d649b0de9beeee6d47
# Parent  a1a316442a9ba33852c0d8e6dcd93a5cdd746baa
tuned output --- less redundancy;

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);