src/Pure/PIDE/markup.ML
changeset 59164 ff40c53d1af9
parent 59125 ee19c92ae8b4
child 59184 830bb7ddb3ab