Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust;
  2. less wasteful consolidation, based on PIDE front-end state and recent changes;
  3. tuned -- short-circuit result;
  4. tuned;
Changeset 68382:b10ae73f0bab by wenzelm:
more robust;
The file was modified src/Pure/PIDE/session.scala (diff)
Changeset 68381:2fd3a6d6ba2e by wenzelm:
less wasteful consolidation, based on PIDE front-end state and recent changes;
The file was modified etc/options (diff)
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/protocol.ML (diff)
The file was modified src/Pure/PIDE/protocol.scala (diff)
The file was modified src/Pure/PIDE/resources.scala (diff)
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/thy_syntax.scala (diff)
Changeset 68380:f249e1f5623b by wenzelm:
tuned -- short-circuit result;
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 68379:1b0ce345d3c8 by wenzelm:
tuned;
The file was modified src/Pure/Concurrent/future.ML (diff)
The file was modified src/Pure/PIDE/execution.ML (diff)