#305 (Jul 13, 2016, 10:11:39 PM)

1. merged (detail / hgweb)
2. misc tuning and modernization; (detail / hgweb)
3. merged (detail / hgweb)
4. misc tuning and modernization; (detail / hgweb)
5. auto indentation of quasi commands; (detail / hgweb)
6. tuned; (detail / hgweb)
7. clarified indentation (amending 37a3fc20154d); (detail / hgweb)
8. tuned; (detail / hgweb)
9. tuned; (detail / hgweb)
10. tuned; (detail / hgweb)
11. clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal; (detail / hgweb)
12. clarified indentation: 'begin' is treated like a separate command without indent; (detail / hgweb)
13. tuned; (detail / hgweb)
14. obsolete; (detail / hgweb)
15. semantic indentation for unstructured proof scripts; (detail / hgweb)
16. misc tuning and modernization; (detail / hgweb)

Started by an SCM change