src/Pure/PIDE/markup.ML
changeset 69968 1a400b14fd3a
parent 69965 da5e7278286b
child 70016 a8142ac5e4b6
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 24 17:45:00 2019 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 24 17:53:46 2019 +0100
     1.3 @@ -78,7 +78,6 @@
     1.4    val fbreakN: string val fbreak: T
     1.5    val itemN: string val item: T
     1.6    val wordsN: string val words: T
     1.7 -  val no_wordsN: string val no_words: T
     1.8    val hiddenN: string val hidden: T
     1.9    val deleteN: string val delete: T
    1.10    val system_optionN: string
    1.11 @@ -433,7 +432,6 @@
    1.12  (* text properties *)
    1.13  
    1.14  val (wordsN, words) = markup_elem "words";
    1.15 -val (no_wordsN, no_words) = markup_elem "no_words";
    1.16  
    1.17  val (hiddenN, hidden) = markup_elem "hidden";
    1.18