src/Pure/PIDE/markup.ML
changeset 62774 cfcb20bbdbd8
parent 62772 77bbe5af41c3
child 62783 75ee05386b90