src/Pure/PIDE/command.ML
changeset 59199 cb8e5f7a5e4a
parent 59193 59f1591a11cb
child 59328 b83d6c3c439a
equal deleted inserted replaced
59198:c73933e07c03 59199:cb8e5f7a5e4a