src/Pure/PIDE/markup.ML
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 *)