#534 (Jan 20, 2018, 12:50:11 AM)

1. merged (detail / hgweb)
2. avoid evaluation of embedded comment; (detail / hgweb)
3. disable "display" style in marginal (line) comment; (detail / hgweb)
4. more uniform output of source / text / theory_text, with handling of formal comments etc.; (detail / hgweb)
5. sort completion result; (detail / hgweb)
6. recovered antiquotation check without latex mode (cf. dfc93f2b01ea); (detail / hgweb)
7. formal treatment of documentation names; (detail / hgweb)
8. support for completion; (detail / hgweb)
9. adapted to a5ca98950a91; (detail / hgweb)
10. tuned output of plain name; (detail / hgweb)
11. clarified signature; (detail / hgweb)
12. tuned; (detail / hgweb)
13. tuned; (detail / hgweb)
14. unused; (detail / hgweb)
15. clarified access to antiquotation options;
    define explicit variants of antiquotations;
    output proper Latex.text;
    misc tuning and clarification; (detail / hgweb)
16. more operations; (detail / hgweb)
17. tuned signature; (detail / hgweb)
18. discontinued unused wrapper: print_mode is provided directly; (detail / hgweb)
19. corrected name (detail / hgweb)
20. moved from AFP/Gromov (detail / hgweb)
21. moved from AFP/Gromov (detail / hgweb)
22. added lemma (detail / hgweb)

Started by an SCM change

This run spent:

• 9.9 sec waiting;
• 1 hr 32 min build duration;
• 1 hr 32 min total from scheduled to completion.