Summary
- output result messages;
- clarified signature;
- more position information;
- more robust check_state loop, even without session activity (e.g. idempotent use_theories);
- synchronized Session.update;
- more interruptible use_theories; tuned comments;
- clarified exception handling: include interrupts;
- support for repeated events;
- tuned;
- more interruptible; tuned signature;
- unload_theories: actually observe required state; misc tuning and clarification;
- tuned signature;
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |
The file was modified | src/Pure/General/pretty.scala (diff) |
The file was modified | src/Pure/Isar/token.scala (diff) |
The file was modified | src/Pure/PIDE/command_span.scala (diff) |
The file was modified | src/Pure/PIDE/document.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Tools/server.scala (diff) |
The file was modified | src/Pure/Concurrent/event_timer.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Tools/server.scala (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |