src/Pure/PIDE/command.ML
changeset 71211 7d522732b7f2
parent 70662 0f9a4e8ee1ab
child 71675 55cb4271858b
equal deleted inserted replaced
71210:66fa99c85095 71211:7d522732b7f2