src/Pure/PIDE/protocol.ML
changeset 82220 cee6d19109e0
parent 78757 a094bf81a496
equal deleted inserted replaced
82197:52290d6ab92d 82220:cee6d19109e0