tuned message;
authorwenzelm
Tue, 09 Apr 2013 12:29:36 +0200
changeset 51653 97de25c51b2d
parent 51640 d022e8bd2375
child 51654 8450b944e58a
tuned message;
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)) =