Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. physical vs. logical events, the latter takes GC time into account; Timeout.apply is based on logical ML time;
  2. misc tuning and clarification;
  3. misc tuning and clarification;
  4. tuned;
  5. updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
  6. dropped junk
Changeset 69826:1bea05713dde by wenzelm:
physical vs. logical events, the latter takes GC time into account;<br>Timeout.apply is based on logical ML time;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
The file was modified src/Pure/Concurrent/timeout.ML (diff)
The file was modified src/Pure/ML/ml_heap.ML (diff)
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 69825:183c345b063e by wenzelm:
misc tuning and clarification;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
Changeset 69824:29c13d8813cb by wenzelm:
misc tuning and clarification;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
Changeset 69823:93784805c6c5 by wenzelm:
tuned;
The file was modified src/Pure/Concurrent/event_timer.ML (diff)
Changeset 69822:8c587dd44f51 by wenzelm:
updated to polyml-5.8-20190220 (pre-release of Poly/ML 5.8);
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified Admin/polyml/README (diff)
The file was modified Admin/polyml/settings (diff)
The file was modified NEWS (diff)
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/ML/ml_statistics.ML (diff)
The file was modified src/Pure/ML/ml_statistics.scala (diff)
Changeset 69821:8432b771f12e by haftmann:
dropped junk
The file was modified src/HOL/Library/Preorder.thy (diff)