tuned markup;
authorwenzelm
Sat, 11 Aug 2012 17:43:00 +0200
changeset 48770 85eeb06ec1c4
parent 48769 e3b7087bb923
child 48771 2ea997196d04
tuned markup;
src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Aug 11 17:40:33 2012 +0200
+++ b/src/Pure/General/symbol_pos.ML	Sat Aug 11 17:43:00 2012 +0200
@@ -70,7 +70,8 @@
       | get_pos ((_, pos) :: _) = Position.str_of pos;
 
     fun err (syms, msg) = fn () =>
-      text () ^ get_pos syms ^ " at " ^ Symbol.beginning 10 (map symbol syms) ^
+      text () ^ get_pos syms ^
+      Markup.markup Isabelle_Markup.no_report (" at " ^ Symbol.beginning 10 (map symbol syms)) ^
       (case msg of NONE => "" | SOME m => "\n" ^ m ());
   in Scan.!! err scan end;