--- a/src/Pure/PIDE/markup.ML Fri Oct 31 22:02:49 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Oct 31 22:09:18 2014 +0100
@@ -118,7 +118,6 @@
val verbatimN: string val verbatim: T
val cartoucheN: string val cartouche: T
val commentN: string val comment: T
- val controlN: string val control: T
val tokenN: string val token: bool -> Properties.T -> T
val keyword1N: string val keyword1: T
val keyword2N: string val keyword2: T
@@ -464,7 +463,6 @@
val (verbatimN, verbatim) = markup_elem "verbatim";
val (cartoucheN, cartouche) = markup_elem "cartouche";
val (commentN, comment) = markup_elem "comment";
-val (controlN, control) = markup_elem "control";
val tokenN = "token";
fun token delimited props = (tokenN, (delimitedN, print_bool delimited) :: props);