src/Pure/PIDE/markup.ML
changeset 78448 573cc2ab69c5
parent 78279 dab089b25eb6
child 78463 c956b43749f0