src/Pure/PIDE/markup.ML
changeset 76730 1b8dd8c0492f
parent 76514 2615cf68f6f4
child 76955 3f25c28c4257
equal deleted inserted replaced
76729:b045b40a65cc 76730:1b8dd8c0492f