src/Pure/PIDE/protocol.ML
changeset 52800 1baa5d19ac44
parent 52786 9795ea654905
child 52808 143f225e50f5