--- a/src/Pure/PIDE/markup.ML Thu Jan 25 14:13:55 2018 +0100
+++ b/src/Pure/PIDE/markup.ML Thu Jan 25 15:21:05 2018 +0100
@@ -71,6 +71,7 @@
val fbreakN: string val fbreak: T
val itemN: string val item: T
val wordsN: string val words: T
+ val no_wordsN: string val no_words: T
val hiddenN: string val hidden: T
val system_optionN: string
val sessionN: string
@@ -393,6 +394,7 @@
(* text properties *)
val (wordsN, words) = markup_elem "words";
+val (no_wordsN, no_words) = markup_elem "no_words";
val (hiddenN, hidden) = markup_elem "hidden";