tuned markup;
authorwenzelm
Sat Mar 15 16:54:32 2014 +0100 (2014-03-15)
changeset 56165dd89ce51d2c8
parent 56164 c7805a88f952
child 56166 9a241bc276cd
tuned markup;
src/Pure/Tools/rail.ML
     1.1 --- a/src/Pure/Tools/rail.ML	Sat Mar 15 15:50:41 2014 +0100
     1.2 +++ b/src/Pure/Tools/rail.ML	Sat Mar 15 16:54:32 2014 +0100
     1.3 @@ -10,6 +10,22 @@
     1.4  
     1.5  (** lexical syntax **)
     1.6  
     1.7 +(* singleton keywords *)
     1.8 +
     1.9 +val keywords =
    1.10 +  Symtab.make [
    1.11 +    ("|", Markup.keyword3),
    1.12 +    ("*", Markup.keyword3),
    1.13 +    ("+", Markup.keyword3),
    1.14 +    ("?", Markup.keyword3),
    1.15 +    ("(", Markup.empty),
    1.16 +    (")", Markup.empty),
    1.17 +    ("\<newline>", Markup.keyword2),
    1.18 +    (";", Markup.keyword2),
    1.19 +    (":", Markup.keyword2),
    1.20 +    ("@", Markup.keyword1)];
    1.21 +
    1.22 +
    1.23  (* datatype token *)
    1.24  
    1.25  datatype kind =
    1.26 @@ -41,7 +57,7 @@
    1.27  
    1.28  fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
    1.29    | reports_of_token (Token ((pos, _), (Keyword, x))) =
    1.30 -      map (pair pos) (Markup.keyword3 :: Completion.suppress_abbrevs x)
    1.31 +      map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
    1.32    | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
    1.33    | reports_of_token _ = [];
    1.34  
    1.35 @@ -67,8 +83,7 @@
    1.36  val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
    1.37  
    1.38  val scan_keyword =
    1.39 -  Scan.one
    1.40 -    (member (op =) ["|", "*", "+", "?", "(", ")", "\<newline>", ";", ":", "@"] o Symbol_Pos.symbol);
    1.41 +  Scan.one (Symtab.defined keywords o Symbol_Pos.symbol);
    1.42  
    1.43  val err_prefix = "Rail lexical error: ";
    1.44