prefer pretty_exn where possible -- NB: low-level General.exnMessage may still be used elsewhere (e.g. by the ML compiler itself);

--- a/src/Pure/Isar/runtime.ML	Mon Apr 08 16:06:54 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Mon Apr 08 17:10:49 2013 +0200
@@ -12,10 +12,11 @@
   exception TOPLEVEL_ERROR
   val debug: bool Unsynchronized.ref
   val exn_context: Proof.context option -> exn -> exn
+  type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}
   type error = ((serial * string) * string option)
-  val exn_messages_ids: (exn -> Position.T) -> exn -> error list
-  val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
-  val exn_message: (exn -> Position.T) -> exn -> string
+  val exn_messages_ids: exn_info -> exn -> error list
+  val exn_messages: exn_info -> exn -> (serial * string) list
+  val exn_message: exn_info -> exn -> string
   val debugging: ('a -> 'b) -> 'a -> 'b
   val controlled_execution: ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
@@ -44,6 +45,7 @@
 
 (* exn_message *)
 
+type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T};
 type error = ((serial * string) * string option);
 
 local
@@ -67,7 +69,7 @@
 
 in
 
-fun exn_messages_ids exn_position e =
+fun exn_messages_ids {exn_position, pretty_exn} e =
   let
     fun raised exn name msgs =
       let val pos = Position.here (exn_position exn) in
@@ -104,7 +106,7 @@
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: if_context context Display.string_of_thm thms)
-            | _ => raised exn (General.exnMessage exn) []);
+            | _ => raised exn (Pretty.string_of (pretty_exn exn)) []);
         in [((i, msg), id)] end)
       and sorted_msgs context exn =
         sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
@@ -113,11 +115,10 @@
 
 end;
 
-fun exn_messages exn_position exn =
-  map #1 (exn_messages_ids exn_position exn);
+fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn);
 
-fun exn_message exn_position exn =
-  (case exn_messages exn_position exn of
+fun exn_message exn_info exn =
+  (case exn_messages exn_info exn of
     [] => "Interrupt"
   | msgs => cat_lines (map snd msgs));
 

--- a/src/Pure/ML/ml_compiler.ML	Mon Apr 08 16:06:54 2013 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Apr 08 17:10:49 2013 +0200
@@ -6,7 +6,6 @@
 
 signature ML_COMPILER =
 sig
-  val exn_position: exn -> Position.T
   val exn_messages_ids: exn -> Runtime.error list
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
@@ -16,10 +15,13 @@
 structure ML_Compiler: ML_COMPILER =
 struct
 
-fun exn_position _ = Position.none;
-val exn_messages_ids = Runtime.exn_messages_ids exn_position;
-val exn_messages = Runtime.exn_messages exn_position;
-val exn_message = Runtime.exn_message exn_position;
+val exn_info =
+ {exn_position = fn _: exn => Position.none,
+  pretty_exn = Pretty.str o General.exnMessage};
+
+val exn_messages_ids = Runtime.exn_messages_ids exn_info;
+val exn_messages = Runtime.exn_messages exn_info;
+val exn_message = Runtime.exn_message exn_info;
 
 fun eval verbose pos toks =
   let

--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Apr 08 16:06:54 2013 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Apr 08 17:10:49 2013 +0200
@@ -17,14 +17,25 @@
     Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   end;
 
+
+(* exn_info *)
+
 fun exn_position exn =
   (case PolyML.exceptionLocation exn of
     NONE => Position.none
   | SOME loc => position_of loc);
 
-val exn_messages_ids = Runtime.exn_messages_ids exn_position;
-val exn_messages = Runtime.exn_messages exn_position;
-val exn_message = Runtime.exn_message exn_position;
+fun pretty_exn (exn: exn) =
+  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));
+
+val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};
+
+
+(* exn_message *)
+
+val exn_messages_ids = Runtime.exn_messages_ids exn_info;
+val exn_messages = Runtime.exn_messages exn_info;
+val exn_message = Runtime.exn_message exn_info;
 
 
 (* parse trees *)
@@ -180,7 +191,7 @@
               (case exn of
                 STATIC_ERRORS () => ""
               | Runtime.TOPLEVEL_ERROR => ""
-              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
+              | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised");
             val _ = output_warnings ();
             val _ = output_writeln ();
           in raise_error exn_msg end;