src/Pure/PIDE/resources.ML
changeset 78434 b4ec7ea073da
parent 77723 b761c91c2447