merged

removed obsolete chmod: isabelle_process no longer supports writable heaps;

redundant -- already provided by Poly/ML toplevel;

prefer bash_process;

only one nested bash process (NB: OS.System = vfork + exec /bin/sh in RTS is faster than Posix.Process.fork/exec in ML);

generalized ML function

tuned bootstrap order to provide type classes in a more sensible order

missing file;

clarified session; tuned headers;

tuned header;

simplified -- always produce heap for RAW, Pure;

merged

isabelle_process executable no longer supports writable heap images;

more careful cleanup;

obsolete;

tuned;

redundant -- already part of Session.finish;

proper exit as in Scala version (in contrast to a45ba78abcc1);

save heap more directly;

clarified modules;

clarified ML heap operations;

generalized

Merge

Merge