Changes

Summary

1. fewer messages;
2. output result messages;
3. clarified signature;
4. more position information;
5. more robust check_state loop, even without session activity (e.g. idempotent use_theories);
6. synchronized Session.update;
7. more interruptible use_theories; tuned comments;
8. clarified exception handling: include interrupts;
9. support for repeated events;
10. tuned;
11. more interruptible; tuned signature;
12. unload_theories: actually observe required state; misc tuning and clarification;
13. tuned signature;