src/Pure/PIDE/protocol.ML
changeset 65333 289561ca4fa3
parent 65300 c262653a3b88
child 65470 a0f49174dbeb