src/Pure/PIDE/protocol.ML
changeset 50503 50f141b34bb7
parent 50500 c94bba7906d2
child 50505 33c92722cc3d