src/Pure/PIDE/protocol.ML
changeset 55003 c65fd9218ea1
parent 54717 42c209a6c225
child 56333 38f1422ef473