src/Pure/PIDE/protocol_message.ML
changeset 76877 c9e091867206
parent 72771 72976a6bd2ba
child 80820 db114ec720cb
equal deleted inserted replaced
76774:2735b11a3de8 76877:c9e091867206