# HG changeset patch
# User wenzelm
# Date 1244315483 -7200
# Node ID ae1a00e1a2f67a4e1bb9cb494c4761bf75669ed0
# Parent  c5d2899b6de96326115aef7dfa16de1a377b72b8
added exn_message (formerly in toplevel.ML);
eval/code: proper Isar runtime support;
tuned signature;

diff -r c5d2899b6de9 -r ae1a00e1a2f6 src/Pure/ML/ml_compiler.ML
--- 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
diff -r c5d2899b6de9 -r ae1a00e1a2f6 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Jun 06 21:11:22 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Jun 06 21:11:23 2009 +0200
@@ -6,7 +6,8 @@
 
 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
 
@@ -31,11 +32,13 @@
     loc_props
   end |> Position.of_properties;
 
-fun exception_position exn =
+fun exn_position exn =
   (case PolyML.exceptionLocation exn of
     NONE => Position.none
   | SOME loc => position_of loc);
 
+val exn_message = Runtime.exn_message exn_position;
+
 
 (* parse trees *)
 
@@ -145,10 +148,13 @@
       end;
 
     fun result_fun (phase1, phase2) () =
-     (case phase1 of NONE => ()
-      | SOME parse_tree => report_parse_tree depth space parse_tree;
-      case phase2 of NONE => err "Static Errors"
-      | SOME code => apply_result (code ()));  (* FIXME cf. Toplevel.program *)
+     ((case phase1 of
+        NONE => ()
+      | SOME parse_tree => report_parse_tree depth space parse_tree);
+      (case phase2 of
+        NONE => err "Static Errors"
+      | SOME code =>
+          apply_result ((code |> Runtime.debugging |> Runtime.toplevel_error exn_message) ())));
 
 
     (* compiler invocation *)