Summary
- merged
- support for Poly/ML entity ids;
- clarified PIDE reports;
- clarified rendering wrt. hyperlinks;
- tuned -- no position;
- clarified focus visibility;
- tuned rendering;
- highlighting of entity def/ref positions wrt. cursor;
- background color for entity def/ref focus;
- tuned;
- more silence;
- avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
- tuned;
- tuned;
- clarified context;
- misc tuning and standardization;
- tuned headers;