# HG changeset patch
# User wenzelm
# Date 1394898872 -3600
# Node ID dd89ce51d2c82ae1c98e0532bab826e5d46c895d
# Parent  c7805a88f9529525b38bb583ac651d98faf0d82c
tuned markup;

diff -r c7805a88f952 -r dd89ce51d2c8 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sat Mar 15 15:50:41 2014 +0100
+++ b/src/Pure/Tools/rail.ML	Sat Mar 15 16:54:32 2014 +0100
@@ -10,6 +10,22 @@
 
 (** lexical syntax **)
 
+(* singleton keywords *)
+
+val keywords =
+  Symtab.make [
+    ("|", Markup.keyword3),
+    ("*", Markup.keyword3),
+    ("+", Markup.keyword3),
+    ("?", Markup.keyword3),
+    ("(", Markup.empty),
+    (")", Markup.empty),
+    ("\<newline>", Markup.keyword2),
+    (";", Markup.keyword2),
+    (":", Markup.keyword2),
+    ("@", Markup.keyword1)];
+
+
 (* datatype token *)
 
 datatype kind =
@@ -41,7 +57,7 @@
 
 fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
   | reports_of_token (Token ((pos, _), (Keyword, x))) =
-      map (pair pos) (Markup.keyword3 :: Completion.suppress_abbrevs x)
+      map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
   | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
   | reports_of_token _ = [];
 
@@ -67,8 +83,7 @@
 val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
 
 val scan_keyword =
-  Scan.one
-    (member (op =) ["|", "*", "+", "?", "(", ")", "\<newline>", ";", ":", "@"] o Symbol_Pos.symbol);
+  Scan.one (Symtab.defined keywords o Symbol_Pos.symbol);
 
 val err_prefix = "Rail lexical error: ";