src/Pure/PIDE/protocol_message.ML
changeset 71693 f249b5c0fea2
parent 71622 ab5009192ebb
child 72771 72976a6bd2ba