#2031 (Oct 13, 2023, 2:44:43 AM)

1. merged (detail / hgweb)
2. prefer Exn.result: avoid accidental capture of interrupts, similar to ML; (detail / hgweb)
3. clarified user errors vs. failures, e.g. java.lang.StackOverflowError; (detail / hgweb)
4. further clarification of Exn.is_interrupt_proper vs. overall Exn.is_interrupt; (detail / hgweb)
5. proper Exn.capture with check_interrupt (amending a3dcae9a2ebe); (detail / hgweb)
6. distinguish proper interrupts from Poly/ML RTS breakdown; (detail / hgweb)
7. tuned; (detail / hgweb)
8. tuned; (detail / hgweb)
9. proper Isabelle_Thread.try_catch; (detail / hgweb)
10. tuned; (detail / hgweb)
11. proper Exn.capture / Isabelle_Thread.try_catch; (detail / hgweb)
12. tuned; (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. proper Exn.capture; (detail / hgweb)
15. more robust: avoid race condition; (detail / hgweb)
16. clarified name; (detail / hgweb)
17. clarified signature; (detail / hgweb)
18. clarified comments; (detail / hgweb)
19. Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts (detail / hgweb)
20. atin now an abbreviation for atin_within, which has been moved to Abstract_Limits (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 54 min waiting;
• 2 hr 3 min build duration;
• 3 hr 58 min total from scheduled to completion.