#1867 (Jan 20, 2023, 12:50:06 AM)

1. merged (detail / hgweb)
2. clarified "selected" status; (detail / hgweb)
3. uniform keywords for embedded syntax; (detail / hgweb)
4. clarified signature; (detail / hgweb)
5. tuned signature; (detail / hgweb)
6. clarified signature; (detail / hgweb)
7. more complete index;
   adhoc page break; (detail / hgweb)
8. tuned comments; (detail / hgweb)
9. parse citations from raw source, without formal context; (detail / hgweb)
10. tuned signature: fewer warnings in IntelliJ IDEA; (detail / hgweb)
11. tuned messages; (detail / hgweb)
12. tuned GUI; (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. more efficient, thanks to persistent lazy data in Document.Node; (detail / hgweb)
15. proper line positions for PIDE document; (detail / hgweb)
16. tuned; (detail / hgweb)
17. HOL/Library/BigO is obsolete (detail / hgweb)
18. merged (detail / hgweb)
19. tidy up of this messy and obsolete theory (detail / hgweb)

Started by an SCM change

This run spent:

• 5.3 sec waiting;
• 1 hr 53 min build duration;
• 1 hr 53 min total from scheduled to completion.