--- 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