#1848 (Dec 28, 2022, 12:50:11 AM)

1. merged (detail / hgweb)
2. clarified modules: avoid duplication; (detail / hgweb)
3. tuned output; (detail / hgweb)
4. support for generic File_Format.parse_data, with persistent result in document model; (detail / hgweb)
5. omit warning: somewhat pointless and out-of-context; (detail / hgweb)
6. clarified signature: avoid case class with mutable state; (detail / hgweb)
7. tuned; (detail / hgweb)
8. clarified signature: more explicit types; (detail / hgweb)
9. merged (detail / hgweb)
10. tidied some messy old proofs (detail / hgweb)

Started by an SCM change

This run spent:

• 9.4 sec waiting;
• 1 hr 52 min build duration;
• 1 hr 52 min total from scheduled to completion.