src/Pure/PIDE/protocol.ML
changeset 72053 4ed33ea8d957
parent 71879 fe7ee970c425
child 72103 7b318273a4aa