src/Pure/PIDE/protocol.ML
changeset 67753 f28aee3ad1e6
parent 67493 c4e9e0c50487
child 68336 09ac56914b29