src/Pure/PIDE/active.ML
changeset 78271 c0dc000d2a40
parent 77778 99a18dcff010