src/Pure/PIDE/protocol_message.ML
changeset 72574 d892f6d66402
parent 71622 ab5009192ebb
child 72771 72976a6bd2ba