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