changeset 69348 | f0aef5e337a2 |
parent 68858 | e1796b8ddbae |
child 70498 | de75eea6ffc8 |
--- 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;