#374 (Aug 14, 2016, 8:15:07 PM)

1. updated NEWS (detail / hgweb)
2. optimized parent computation in MaSh (detail / hgweb)
3. avoid loading MaSh file first time around for higher responsiveness of Sledgehammer (detail / hgweb)
4. tuned MaSh's metacharacters to avoid needless decoding (detail / hgweb)
5. optimization in MaSh parsing (detail / hgweb)
6. tuned ML (detail / hgweb)
7. removed trailing final stops in Nitpick messages (detail / hgweb)
8. killed final stops in Sledgehammer and friends (detail / hgweb)
9. tuned message (detail / hgweb)
10. tuning punctuation in messages output by Isabelle (detail / hgweb)
11. tuning whitespace in output syntax (detail / hgweb)

Started by an SCM change