--- a/src/Pure/Isar/token.ML Fri Oct 31 22:02:49 2014 +0100
+++ b/src/Pure/Isar/token.ML Fri Oct 31 22:09:18 2014 +0100
@@ -199,7 +199,7 @@
in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end;
-(* control tokens *)
+(* stopper *)
fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
val eof = mk_eof Position.none;
@@ -300,7 +300,7 @@
| Comment => (Markup.comment, "")
| InternalValue => (Markup.empty, "")
| Error msg => (Markup.bad, msg)
- | EOF => (Markup.control, "");
+ | EOF => (Markup.empty, "");
in
--- a/src/Pure/ML/ml_lex.ML Fri Oct 31 22:02:49 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Fri Oct 31 22:09:18 2014 +0100
@@ -73,7 +73,7 @@
fun end_pos_of (Token ((_, pos), _)) = pos;
-(* control tokens *)
+(* stopper *)
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
val eof = mk_eof Position.none;
--- 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);