# HG changeset patch
# User wenzelm
# Date 1344092815 -7200
# Node ID 9bc7922ba2ae2179b7569e1e1c5f34cf1541fac6
# Parent  951bc4c3ee173e007b76eea2def8d86e8b760070
further robustification of interrupts during build;

diff -r 951bc4c3ee17 -r 9bc7922ba2ae src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Sat Aug 04 16:56:42 2012 +0200
+++ b/src/Pure/System/build.ML	Sat Aug 04 17:06:55 2012 +0200
@@ -55,30 +55,31 @@
 
 in
 
-fun build args_file =
-  let
-    val (do_output, (options, (verbose, (browser_info, (parent_name,
-        (name, theories)))))) =
-      File.read (Path.explode args_file) |> YXML.parse_body |>
-        let open XML.Decode in
-          pair bool (pair Options.decode (pair bool (pair string (pair string
-            (pair string ((list (pair Options.decode (list string)))))))))
-        end;
+fun build args_file = uninterruptible (fn restore_attributes => fn () =>
+  restore_attributes (fn () =>
+    let
+      val (do_output, (options, (verbose, (browser_info, (parent_name,
+          (name, theories)))))) =
+        File.read (Path.explode args_file) |> YXML.parse_body |>
+          let open XML.Decode in
+            pair bool (pair Options.decode (pair bool (pair string (pair string
+              (pair string ((list (pair Options.decode (list string)))))))))
+          end;
 
-    val _ =
-      Session.init do_output false
-        (Options.bool options "browser_info") browser_info
-        (Options.string options "document")
-        (Options.bool options "document_graph")
-        (space_explode ":" (Options.string options "document_variants"))
-        parent_name name
-        (Options.string options "document_dump",
-          Present.dump_mode (Options.string options "document_dump_mode"))
-        "" verbose;
-    val _ = Session.with_timing name verbose (List.app use_theories) theories;
-    val _ = Session.finish ();
-    val _ = if do_output then () else quit ();
-  in () end
+      val _ =
+        Session.init do_output false
+          (Options.bool options "browser_info") browser_info
+          (Options.string options "document")
+          (Options.bool options "document_graph")
+          (space_explode ":" (Options.string options "document_variants"))
+          parent_name name
+          (Options.string options "document_dump",
+            Present.dump_mode (Options.string options "document_dump_mode"))
+          "" verbose;
+      val _ = Session.with_timing name verbose (List.app use_theories) theories;
+      val _ = Session.finish ();
+      val _ = if do_output then () else quit ();
+    in () end) ()) ()
   handle exn =>
     (Output.error_msg (ML_Compiler.exn_message exn);
      if Exn.is_interrupt exn then exit 130 else exit 1);