# HG changeset patch
# User wenzelm
# Date 1543332132 -3600
# Node ID f0aef5e337a2d1f8c7d2c830955452124e6a97f8
# Parent  54b95d2ec0400f45b3f8b4863eac06f00555b2f3
more robust (amending 76979adf0b96);

diff -r 54b95d2ec040 -r f0aef5e337a2 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Nov 27 16:20:08 2018 +0100
+++ b/src/Pure/General/position.ML	Tue Nov 27 16:22:12 2018 +0100
@@ -238,7 +238,7 @@
       | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
       | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
   in
-    if null props then ""
+    if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;