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);
1.1 --- a/src/Pure/System/session.ML Fri Dec 07 23:11:01 2012 +0100
1.2 +++ b/src/Pure/System/session.ML Fri Dec 07 23:14:39 2012 +0100
1.3 @@ -79,6 +79,7 @@
1.4 Keyword.status ();
1.5 Outer_Syntax.check_syntax ();
1.6 Options.reset_default ();
1.7 + Future.shutdown ();
1.8 session_finished := true);
1.9
1.10