--- 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