more robust (amending 76979adf0b96);

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