src/Pure/PIDE/protocol.ML
changeset 74266 612b7e0d6721
parent 73559 22b5ecb53dd9
child 74671 df12779c3ce8