# HG changeset patch
# User wenzelm
# Date 1365503376 -7200
# Node ID 97de25c51b2df954930077c058ea096f632dd9ed
# Parent  d022e8bd2375387f60ac94d023e5f27479055bc2
tuned message;

diff -r d022e8bd2375 -r 97de25c51b2d src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Mon Apr 08 21:01:59 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Tue Apr 09 12:29:36 2013 +0200
@@ -76,7 +76,9 @@
         (case msgs of
           [] => "exception " ^ name ^ " raised" ^ pos
         | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
-        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
+        | _ =>
+            cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") ::
+              map (Markup.markup Markup.item) msgs))
       end;
 
     fun exn_msgs (context, ((i, exn), id)) =