#1748 (Aug 14, 2022, 12:51:09 AM)

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

Started by an SCM change

This run spent:

• 8.3 sec waiting;
• 1 hr 48 min build duration;
• 1 hr 48 min total from scheduled to completion.