Implement multi-session support for Holmake etc

[mn200]

We should gain a deal of build-time efficiency by having multiple theories built within the one Poly/ML session. It's even possible that

val _ = export_theory()  (* end of theory 1 *)
val _ = new_theory "theory2"

currently does something reasonable. There would probably need to be special syntax to suggest to Holmake that such a linear sequence of calls would work. I'm very confident though that it would be a great deal of work to get builds that weren't linear descents through the hierarchy to work.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.