Summary
- more options;
- allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
- tuned;
- tuned signature;
The file was modified | src/Pure/Tools/server_commands.scala (diff) |
The file was modified | src/Pure/Thy/sessions.scala (diff) |
The file was modified | src/Pure/Thy/thy_resources.scala (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |
The file was modified | src/Tools/VSCode/src/protocol.scala (diff) |
The file was modified | src/Pure/General/json.scala (diff) |
The file was modified | src/Pure/Tools/server.scala (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |
The file was modified | src/Tools/VSCode/src/protocol.scala (diff) |