src/Pure/PIDE/command.ML
changeset 76730 1b8dd8c0492f
parent 76436 9e5098cbf81f
child 76803 5ffe32b613ae