Skip to content
Success

Changes

Summary

  1. proper graph traversal: avoid multiple visit of unnamed nodes;
  2. more scalable: avoid huge intermediate XML elems;
  3. more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
Changeset 70602:b85a12c2e2bf by wenzelm:
proper graph traversal: avoid multiple visit of unnamed nodes;
The file was modified src/Pure/Thy/thm_deps.ML (diff)
Changeset 70601:79831e40e2be by wenzelm:
more scalable: avoid huge intermediate XML elems;
The file was modified src/Pure/General/buffer.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 70600:6e97e31933a6 by wenzelm:
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/General/buffer.ML (diff)