make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
authorwenzelm
Fri, 07 Dec 2012 23:14:39 +0100
changeset 50430 702278df3b57
parent 50429 f8cd5e53653b
child 50431 955c4aa44f60
child 50434 960a3429615c
make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Fri Dec 07 23:11:01 2012 +0100
+++ b/src/Pure/System/session.ML	Fri Dec 07 23:14:39 2012 +0100
@@ -79,6 +79,7 @@
   Keyword.status ();
   Outer_Syntax.check_syntax ();
   Options.reset_default ();
+  Future.shutdown ();
   session_finished := true);