support for more informative crashes;

Isabelle-hg: http://isabelle.in.tum.de/repos/isabelle@51980 fe16d1128a14857b47f355487a59328efe65746b
more scalable Library.separate -- NB: JVM has tiny fixed-size stack;

Isabelle-hg: http://isabelle.in.tum.de/repos/isabelle@51981 a8ffd3692f57e4693ef854e11e08a602e3e8cf0b
more scalable File.write via separate chunks;
tuned signature of File.write_xz: prefer defaults over overloading;

Isabelle-hg: http://isabelle.in.tum.de/repos/isabelle@51982 fb4352e89022c78550a3edf0657dcba176a56ca7
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);

Isabelle-hg: http://isabelle.in.tum.de/repos/isabelle@51983 32692ce4c61aff48dfd2e12cbf1323175285f0c3
more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError;

Isabelle-hg: http://isabelle.in.tum.de/repos/isabelle@51986 5fdca5bfc0b4644fb2a96aced644fc52d7e485ea
tuned signature;

Isabelle-hg: http://isabelle.in.tum.de/repos/isabelle@51987 7d8e0e3c553b308cf54fcefd3c8c98d0712bebdd