collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems);

--- a/src/Pure/System/build.ML	Thu Oct 18 13:53:02 2012 +0200
+++ b/src/Pure/System/build.ML	Thu Oct 18 13:57:27 2012 +0200
@@ -88,13 +88,16 @@
           (Options.string options "document_dump",
             Present.dump_mode (Options.string options "document_dump_mode"))
           "" verbose;
-      val _ =
+
+      val res1 =
         theories |>
           (List.app use_theories
             |> Session.with_timing name verbose
-            |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads"));
+            |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
+            |> Exn.capture);
+      val res2 = Exn.capture Session.finish ();
+      val _ = Par_Exn.release_all [res1, res2];
 
-      val _ = Session.finish ();
       val _ = if do_output then () else exit 0;
     in 0 end);
 

--- a/src/Pure/System/session.ML	Thu Oct 18 13:53:02 2012 +0200
+++ b/src/Pure/System/session.ML	Thu Oct 18 13:57:27 2012 +0200
@@ -67,16 +67,16 @@
 (* finish *)
 
 fun finish () =
-  (Thy_Info.finish ();
-    Present.finish ();
-    Keyword.status ();
-    Outer_Syntax.check_syntax ();
-    Future.shutdown ();
-    Goal.finish_futures ();
-    Goal.cancel_futures ();
-    Future.shutdown ();
-    Options.reset_default ();
-    session_finished := true);
+ (Future.shutdown ();
+  Goal.finish_futures ();
+  Thy_Info.finish ();
+  Present.finish ();
+  Keyword.status ();
+  Outer_Syntax.check_syntax ();
+  Goal.cancel_futures ();
+  Future.shutdown ();
+  Options.reset_default ();
+  session_finished := true);
 
 
 (* use_dir *)
@@ -124,12 +124,16 @@
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
-     (Output.physical_stderr
-        "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
-      init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
-        (doc_dump dump) rpath verbose;
-      with_timing item timing use root;
-      finish ()))
+    let
+      val _ =
+        Output.physical_stderr
+          "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
+      val _ =
+        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
+          (doc_dump dump) rpath verbose;
+      val res1 = (use |> with_timing item timing |> Exn.capture) root;
+      val res2 = Exn.capture finish ();
+    in ignore (Par_Exn.release_all [res1, res2]) end)
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
     |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs