src/Pure/PIDE/command.ML
changeset 54554 b8d0d8407c3b
parent 54527 bfeb0ea6c2c0
child 54671 d64a4ef26edb