src/Pure/PIDE/protocol_message.ML
changeset 81864 17831ae5224d
parent 80820 db114ec720cb