Changes

Summary

1. more direct hg_sync init via ssh (see also 721b3278c8e4);
2. tuned;
3. more operations;
4. tuned: more direct re-use;
5. more direct clone (see also change of exception in 8d8c70b41bab);
6. more operations, following Isabelle/ML conventions;
7. more operations, following Isabelle/ML conventions;
8. proforma use of Long_Name.chunks, without change of the representation of accesses yet;
9. merged
10. minor performance tuning;
11. compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
12. clarified signature;
13. misc tuning and clarification;
14. more compact: avoid redundant entries;
15. tuned;
16. tuned;
17. more operations;
18. performance tuning: proper pointer_eq;