Summary
- merged
- more careful PIDE reports: avoid duplicates, notably in situation of backtracking loops;
- avoid multiple PIDE markup due to (potentially infinite) backtracking;
- more permissive remote_build_history: failure happens routinely and should not lead error, without saving logs;
The file was modified | src/Pure/Isar/token.ML (diff) |
The file was modified | src/Pure/Isar/proof.ML (diff) |
The file was modified | src/Pure/Admin/build_history.scala (diff) |