Changes

Summary

1. merged
2. template for $ISABELLE_HOME_USER/ROOTS;
3. tuned;
4. clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);
5. reverted 6acb28e5ba41: permissiveness of 1e5ae735e026 should be sufficient;
6. tuned;
7. tolerate errors in session structure, although this may lead to confusion about theory imports later on;
8. clarified errors;
9. clarified signature; tuned ssh.prefix;
10. tuned;