src/Pure/PIDE/markup.ML
changeset 53634 ab5d01b69a07
parent 53378 07990ba8c0ea
child 54702 3daeba5130f0
equal deleted inserted replaced
53631:e68732cd842e 53634:ab5d01b69a07