src/Pure/General/position.ML
changeset 55546 76979adf0b96
parent 54038 f522477d671d
child 55624 d52409077135
--- 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