Changes

Summary

1. optional notification of nodes_status (via progress); more accurate changed.nodes wrt. dep_theories; tuned signature;
2. tuned signature;
3. tuned;
4. tuned;
5. tuned signature;
6. tuned output;
7. clarified signature;
8. clarified signature;
9. clarified signature;
10. trim nodes_status: avoid potential memory leak;
11. simplified (cf. dcd69422b953);
12. clarified modules;
13. clarified modules;