src/Pure/PIDE/protocol.ML
changeset 79202 626d00cb4d9c
parent 78757 a094bf81a496