src/Pure/PIDE/markup.ML
changeset 82475 0a6d57c4d58b
parent 82316 83584916b6d7
equal deleted inserted replaced
82474:fcefbef691bf 82475:0a6d57c4d58b