src/Pure/PIDE/protocol_message.ML
changeset 72279 ae89eac1d332
parent 71622 ab5009192ebb
child 72771 72976a6bd2ba
equal deleted inserted replaced
72271:7e90e1d178b5 72279:ae89eac1d332