Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
  3. avoid multiple PIDE markup due to (potentially infinite) backtracking;
  4. more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
Changeset 64422:efdd4c5daf7d by wenzelm:
merged
Changeset 64421:681fae6b00b5 by wenzelm:
more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
The file was modified src/Pure/Isar/token.ML (diff)
Changeset 64420:2efc128370fa by wenzelm:
avoid multiple PIDE markup due to (potentially infinite) backtracking;
The file was modified src/Pure/Isar/proof.ML (diff)
Changeset 64419:0f3b0a929c02 by wenzelm:
more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
The file was modified src/Pure/Admin/build_history.scala (diff)