Changes

Summary

1. tuned comments;
2. tuned signature;
3. clarified signature;
4. clarified signature;
5. clarified signature;
6. unused;
7. clarified modules;
8. clarified signature;
9. clarified signature: more explicit types;
10. clarified signature --- avoid dependent types;
11. tuned whitespace;
12. clarified signature: avoid public representation;
13. tuned signature;
14. clarified signature;
15. unused;
16. more accurate treatment of option "editor_output_state", e.g. when changed via Isabelle/jEdit Plugin Options panel;
17. clarified signature: more explicit types; more robust zoom.factor: work with uninitialized GUI components;
18. tuned whitespace;
19. tuned, following 298707451ec2; tuned signature;
20. unused;
21. tuned, following hints by IntelliJ IDEA;
22. clarified signature: more explicit types; tuned whitespace;
23. tuned whitespace;
24. tuned, following hints by IntelliJ IDEA;