Changes

Summary

1. merged
2. support for Poly/ML entity ids;
3. clarified PIDE reports;
4. clarified rendering wrt. hyperlinks;
5. tuned -- no position;
6. clarified focus visibility;
7. tuned rendering;
8. highlighting of entity def/ref positions wrt. cursor;
9. background color for entity def/ref focus;
10. tuned;
11. more silence;
12. avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
13. tuned;
14. tuned;
15. clarified context;
16. misc tuning and standardization;
17. tuned headers;