#886 (Mar 11, 2019, 1:15:00 AM)

1. more formal contributors (with the help of the history); (detail / hgweb)
2. proper data columns for plots; (detail / hgweb)
3. merged (detail / hgweb)
4. tuned -- Toplevel.presentation_context is total; (detail / hgweb)
5. document markers are formal comments, and may thus occur anywhere in the command-span;
   clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
   tuned signature; (detail / hgweb)
6. PIDE markup for spell-checking; (detail / hgweb)
7. markup and document markers for some meta data from "Dublin Core Metadata Element Set"; (detail / hgweb)
8. tuned; (detail / hgweb)
9. added semantic document markers;
   emulate old-style tags as "tag" markers, with subtle change of semantics for multiples tags (ever used?);
   tuned; (detail / hgweb)
10. clarified signature; (detail / hgweb)
11. added glyph for \<marker>; (detail / hgweb)
12. tuned proof; (detail / hgweb)
13. clarified Toplevel.state: more explicit types;
    presentation context is always present, with default to Pure.thy and fall-back to Pure bootstrap theory; (detail / hgweb)
14. tuned; (detail / hgweb)
15. merged (detail / hgweb)
16. tidied up HOL/ex/Primrec (detail / hgweb)

Started by an SCM change

This run spent:

• 24 min waiting;
• 1 hr 29 min build duration;
• 1 hr 54 min total from scheduled to completion.