src/Pure/PIDE/protocol_message.ML
changeset 76371 1ac2416e8432
parent 72771 72976a6bd2ba
child 80820 db114ec720cb
equal deleted inserted replaced
76370:9bd948666e8a 76371:1ac2416e8432