src/Pure/PIDE/resources.ML
changeset 76853 e37c58cbb79f
parent 76818 947510ce4e36
child 76880 6a07cf09604d