Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
primitive use_text: let interrupts pass unhindered;
authorwenzelm
Fri, 10 Sep 2010 12:39:20 +0200
changeset 39242 28d3809ff91f
parent 39241 e9a442606db3
child 39243 307e3d07d19f
primitive use_text: let interrupts pass unhindered;
src/Pure/ML-Systems/compiler_polyml-5.2.ML file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/compiler_polyml-5.3.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Thu Sep 09 21:30:33 2010 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Fri Sep 10 12:39:20 2010 +0200
@@ -37,8 +37,10 @@
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
-       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        error (output ()); reraise exn);
+        if Exn.is_interrupt exn then reraise exn
+        else
+         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+          error (output ()); reraise exn);
   in if verbose then print (output ()) else () end;
 
 fun use_file context verbose name =
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Sep 09 21:30:33 2010 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Fri Sep 10 12:39:20 2010 +0200
@@ -41,8 +41,10 @@
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
-       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        error (output ()); reraise exn);
+        if Exn.is_interrupt exn then reraise exn
+        else
+         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+          error (output ()); reraise exn);
   in if verbose then print (output ()) else () end;
 
 fun use_file context verbose name =
isabelle