src/Pure/PIDE/protocol.ML
changeset 72047 b9e9ff3a1e1c
parent 71879 fe7ee970c425
child 72103 7b318273a4aa