# HG changeset patch
# User wenzelm
# Date 1414789758 -3600
# Node ID 2885e2eaa0fb22eb612e2f216764163e45c9e40d
# Parent  b979c781c2dbf1df5f56bcc93efdfed0c709badb
removed pointless markup;
tuned comments;

diff -r b979c781c2db -r 2885e2eaa0fb src/Pure/Isar/token.ML
--- 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
 
diff -r b979c781c2db -r 2885e2eaa0fb src/Pure/ML/ml_lex.ML
--- 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;
diff -r b979c781c2db -r 2885e2eaa0fb src/Pure/PIDE/markup.ML
--- 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);