Summary
- proper graph traversal: avoid multiple visit of unnamed nodes;
- more scalable: avoid huge intermediate XML elems;
- more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
The file was modified | src/Pure/Thy/thm_deps.ML (diff) |
The file was modified | src/Pure/General/buffer.ML (diff) |
The file was modified | src/Pure/Thy/export_theory.ML (diff) |
The file was modified | src/Pure/General/buffer.ML (diff) |