src/Pure/PIDE/markup.ML
changeset 56275 600f432ab556
parent 56202 0a11d17eeeff
child 56278 2576d3a40ed6