Changes

Summary

1. merged
2. First round of moving material from the number theory development
3. merged
4. more GUI operations;
5. proper handling of state updates;
6. clarified process management;
7. tuned signature;
8. clarified state document nodes for Theories_Status / Document_Dockable;
9. clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
10. tuned whitespace;
11. clarified module initialization;
12. tuned signature, following Document_Dockable;
13. tuned signature;
14. clarified GUI;
15. tuned signature;
16. proper thread context;
17. more informative errors, including optional Exn.trace;
18. clarified state change: presumably more robust;
19. proper state change, e.g. on open/close of "Document" panel;
20. clarified module initialization;
21. clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
22. clarified signature;
23. tuned signature;
24. added lifting_forget as suggested by Peter Lammich