| changeset 68298 | 2c3ce27cf4a8 | 
| parent 68101 | 0699a0bacc50 | 
| child 68323 | bf7336731981 | 
--- a/src/Pure/PIDE/markup.ML Sat May 26 22:12:18 2018 +0100 +++ b/src/Pure/PIDE/markup.ML Sun May 27 13:42:01 2018 +0200 @@ -73,6 +73,7 @@ val wordsN: string val words: T val no_wordsN: string val no_words: T val hiddenN: string val hidden: T + val deleteN: string val delete: T val system_optionN: string val sessionN: string val theoryN: string @@ -402,6 +403,8 @@ val (hiddenN, hidden) = markup_elem "hidden"; +val (deleteN, delete) = markup_elem "delete"; + (* misc entities *)