#1470 (May 24, 2021, 12:50:10 AM)

1. further "unset CDPATH", whenever a new non-interactive bash is started (see also ac07f6be27ea); (detail / hgweb)
2. merged (detail / hgweb)
3. NEWS; (detail / hgweb)
4. clarified index, more like formal @{element_ref}; (detail / hgweb)
5. clarified treatment of type constructors; (detail / hgweb)
6. misc tuning and clarification; (detail / hgweb)
7. tuned signature; (detail / hgweb)
8. clarified context; (detail / hgweb)
9. more uniform document antiquotations for ML: consolidate former setup for manuals; (detail / hgweb)
10. clarified names; (detail / hgweb)
11. clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; (detail / hgweb)
12. clarified modules; (detail / hgweb)
13. clarified modules; (detail / hgweb)
14. tuned; (detail / hgweb)
15. clarified signature: avoid dispatch via name; (detail / hgweb)
16. clarified, e.g. type variables; (detail / hgweb)
17. tuned index; (detail / hgweb)
18. more ambitious default for index "is like"; (detail / hgweb)
19. tuned; (detail / hgweb)
20. support for index entries; (detail / hgweb)
21. tuned; (detail / hgweb)
22. tuned signature; (detail / hgweb)
23. clarified modules; (detail / hgweb)
24. clarified old document build; (detail / hgweb)
25. unused; (detail / hgweb)
26. prefer standard document_build=lualatex --- ISABELLE_TMP/examples has been removed already in 435fb018e8ee; (detail / hgweb)
27. prefer standard document_build=lualatex --- no impact of "sedindex" in prepare_document; (detail / hgweb)
28. unused; (detail / hgweb)
29. proper Unix lines; (detail / hgweb)
30. prefer explicit option document_bibliography (actually ignored by build script); (detail / hgweb)
31. explicit option document_bibliography; (detail / hgweb)
32. proper bibliography; (detail / hgweb)
33. discontinued obsolete "isabelle latex"; (detail / hgweb)
34. more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
    clarified ISABELLE_MAKEINDEX options; (detail / hgweb)
35. default document_build (lualatex); (detail / hgweb)
36. more robust: allow \printindex within the document; (detail / hgweb)
37. clarified bash scripts, with public interfaces for user-defined Document_Build.Engine; (detail / hgweb)
38. tuned signature; (detail / hgweb)
39. option document_preprocessor; (detail / hgweb)
40. show symbols in Isabelle/ML instead of perl; (detail / hgweb)
41. more robust run of makeindex (amending 0f0a2148a099, Gerwin Klein 2004), using the old status-quo of e.g. doc-src/Intro/Makefile; (detail / hgweb)
42. tuned --- more robust; (detail / hgweb)
43. discontinued somewhat pointless "fixbookmarks": default output works sufficiently well; (detail / hgweb)
44. more uniform bibtex error, without using perl (see 4710dd5093a3); (detail / hgweb)
45. proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error); (detail / hgweb)
46. tuned; (detail / hgweb)
47. clarified command-line options; (detail / hgweb)
48. obsolete (see 5a3a2a52648d); (detail / hgweb)
49. redundant: copy produced from session document_files; (detail / hgweb)
50. clarified treatment of Isabelle .sty files; (detail / hgweb)
51. option document_logo; (detail / hgweb)
52. proper options; (detail / hgweb)
53. option document_build refers to build engine in Isabelle/Scala;
    pdflatex is back as legacy build engine, e.g. for published proceedings; (detail / hgweb)
54. redundant: tmp_dir is purged anyway; (detail / hgweb)
55. misc tuning and clarification; (detail / hgweb)
56. clarified modules; (detail / hgweb)
57. tuned --- clarified corner cases; (detail / hgweb)
58. more uniform use of Properties.Eq.unapply, with slightly changed semantics in boundary cases; (detail / hgweb)
59. clarified signature -- avoid odd warning about scala/bug#6675; (detail / hgweb)
60. tuned; (detail / hgweb)
61. tuned; (detail / hgweb)
62. clarified signature; (detail / hgweb)
63. proper syntax of Scala 3; (detail / hgweb)
64. enforce syntax of Scala 3; (detail / hgweb)

Started by an SCM change

This run spent:

• 8.7 sec waiting;
• 1 hr 27 min build duration;
• 1 hr 27 min total from scheduled to completion.