Summary
- guard result exports via export_pattern -- avoid bombing client via huge blobs;
- tuned;
- clarified output: avoid costly operations on huge blobs;
- unused;
- more scalable -- avoid huge lines within stdout;
- slightly more ambitious parallelism (again);
- more scalable API;
The file was modified | src/Doc/System/Server.thy (diff) |
The file was modified | src/Doc/System/Sessions.thy (diff) |
The file was modified | src/Pure/Tools/server_commands.scala (diff) |
The file was modified | src/Pure/Thy/export.scala (diff) |
The file was modified | src/Pure/General/bytes.scala (diff) |
The file was modified | src/Pure/General/bytes.scala (diff) |
The file was modified | src/Pure/library.ML (diff) |
The file was modified | src/Pure/PIDE/markup.scala (diff) |
The file was modified | src/Pure/Tools/build.ML (diff) |
The file was modified | src/Pure/Tools/build.scala (diff) |
The file was modified | src/Pure/Concurrent/future.ML (diff) |
The file was modified | src/Pure/Thy/export.ML (diff) |