Changes

Summary

1. removed old proof method "default";
2. clean message more thoroughly;
3. clarified modules; removed unsed exn_id;
4. avoid interference with running PIDE protocol;
5. proper signature for structure; tuned;
6. tuned signature; proper signature for structure;
7. proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
8. support ROOT0.ML as well -- independently of ROOT.ML;
9. flags as in 'ML' command;
10. shared output primitives of physical/virtual Pure;
11. shared thread position for physical/virtual Pure;
12. prefer Synchronized.var;
13. tuned signature;
14. virtual Pure is single-threaded to avoid confusion with multiple thread farms etc.;
15. tuned signature;
16. tuned signature -- closer to Exn.Interrupt.expose in Scala;
17. clarified bootstrap;
18. clarified context; avoid Unsynchronized.ref;
19. old;
20. ensure globally unique counter results;
21. tuned;
22. clarified modules;