# HG changeset patch
# User wenzelm
# Date 1244625126 -7200
# Node ID 3371a3c19bb169bace980e060f9f2eeec7bc4115
# Parent  4ed9d9dc17ee6fe028757cbff1651c0b5b16fb1b
reraise exceptions to preserve position information;

diff -r 4ed9d9dc17ee -r 3371a3c19bb1 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Jun 10 00:46:37 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Wed Jun 10 11:12:06 2009 +0200
@@ -223,7 +223,7 @@
 
 fun the_struct structs i =
   if 1 <= i andalso i <= length structs then nth structs (i - 1)
-  else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
+  else error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
       Lexicon.free (the_struct structs 1)
@@ -503,7 +503,7 @@
     val exn_results = map (Exn.capture ast_of) pts;
     val exns = map_filter Exn.get_exn exn_results;
     val results = map_filter Exn.get_result exn_results
-  in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
+  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
 
 
 
@@ -534,6 +534,6 @@
     val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
     val exns = map_filter Exn.get_exn exn_results;
     val results = map_filter Exn.get_result exn_results
-  in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
+  in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
 
 end;
diff -r 4ed9d9dc17ee -r 3371a3c19bb1 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Jun 10 00:46:37 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jun 10 11:12:06 2009 +0200
@@ -387,7 +387,7 @@
     (case Graph.get_node tasks name of
       Task body =>
         let val after_load = body ()
-        in after_load () handle exn => (kill_thy name; raise exn) end
+        in after_load () handle exn => (kill_thy name; reraise exn) end
     | _ => ()));
 
 in