src/Pure/PIDE/command.ML
changeset 72215 8f9cffa78112
parent 71675 55cb4271858b
child 72747 5f9d66155081