Changes

Summary

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