src/Pure/ML/ml_compiler.ML
changeset 31477 ae1a00e1a2f6
parent 31428 3b32a57b044b
child 38874 4a4d34d2f97b
--- a/src/Pure/ML/ml_compiler.ML	Sat Jun 06 21:11:22 2009 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Sat Jun 06 21:11:23 2009 +0200
@@ -6,14 +6,16 @@
 
 signature ML_COMPILER =
 sig
-  val exception_position: exn -> Position.T
+  val exn_position: exn -> Position.T
+  val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
 structure ML_Compiler: ML_COMPILER =
 struct
 
-fun exception_position _ = Position.none;
+fun exn_position _ = Position.none;
+val exn_message = Runtime.exn_message exn_position;
 
 fun eval verbose pos toks =
   let