src/Pure/PIDE/protocol.ML
changeset 46980 6bc213e90401
parent 46938 cda018294515
child 47343 b8aeab386414