Skip to content
Success

Changes

Summary

  1. tuned;
  2. tuned;
  3. add root entry for non-local components;
  4. clarified;
  5. extra timer delay, to limit db transactions;
  6. proper synchronized;
  7. clarified ternary tries
The file was modified src/Pure/Build/build_manager.scala (diff)
The file was modified src/Pure/Build/build_manager.scala (diff)
Changeset 80408:e6d3d1db6136 by fabian huch _huch@in.tum.de_:
add root entry for non-local components;
The file was modified src/Pure/Build/build_manager.scala (diff)
The file was modified src/Pure/Build/build_manager.scala (diff)
Changeset 80406:d85ad13d8cf3 by fabian huch _huch@in.tum.de_:
extra timer delay, to limit db transactions;
The file was modified etc/options (diff)
The file was modified src/Pure/Build/build_manager.scala (diff)
Changeset 80405:661a226bb49a by fabian huch _huch@in.tum.de_:
proper synchronized;
The file was modified src/Pure/Build/build_manager.scala (diff)
Changeset 80404:f34e62eda167 by nipkow:
clarified ternary tries
The file was addedsrc/HOL/Data_Structures/Trie_Ternary.thy
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Data_Structures/Trie_Map.thy