Changes

Summary

1. merged
2. support for dynamic document output while editing;
3. adjust position according to offset of command/exec id;
4. tuned signature (see Command.eval_state);
5. export generated document.tex, unless explicit document=false;
6. more general presentation hook, with document preparation as application;
7. clarified signature: more explicit type "context" with full options;
8. more explicit type Thy_Output.segment;
9. clarified signature; more operations;
10. more sorted cleaning
11. cleaning up sorted