--- a/src/Pure/General/position.ML Mon Feb 17 20:54:03 2014 +0100
+++ b/src/Pure/General/position.ML Mon Feb 17 21:37:41 2014 +0100
@@ -192,7 +192,7 @@
(SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
| (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
| (NONE, SOME name) => "(file " ^ quote name ^ ")"
- | _ => "");
+ | _ => if is_reported pos then "\\<here>" else "");
in
if null props then ""
else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s