src/Pure/PIDE/protocol_message.ML
changeset 72047 b9e9ff3a1e1c
parent 71622 ab5009192ebb
child 72771 72976a6bd2ba
equal deleted inserted replaced
72046:c386d1b77762 72047:b9e9ff3a1e1c