Changes

Summary

1. more informative error;
2. proper else statement;
3. tuned;
4. clarified session log file: avoid erratic messages;
5. clarified messages;
6. clarified messages;
7. NEWS and documentation for "isabelle log";
8. clarified messages;
9. clarified types;
10. clarified Pretty.Metric, as for build errors;
11. clarified types;
12. tuned;
13. clarified: omit presumably pointless Markup.Serial (see also 0b9334adcf05);
14. clarified signature: more specific types;
15. tuned messages;
16. clarified output of Isabelle symbols;
17. tuned signature;
18. clarified file sources: take from build database instead of file-system;
19. tuned;
20. tuned messages;