src/Pure/PIDE/markup.ML
changeset 60916 a6e2a667b0a8
parent 60842 5510c8444bc4
child 61209 7a421e7ef97c
equal deleted inserted replaced
60915:2986137093c6 60916:a6e2a667b0a8