# HG changeset patch
# User wenzelm
# Date 1695548533 -7200
# Node ID 5fe4c11b5ecbeb957d084cee1424535f918eb58a
# Parent  c37f2eb8d038d83d9a1763041d9d573710dd512d
minor performance tuning;

diff -r c37f2eb8d038 -r 5fe4c11b5ecb src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sat Sep 23 18:45:28 2023 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Sep 24 11:42:13 2023 +0200
@@ -55,11 +55,11 @@
   "type", "val", "where", "while", "with", "withtype"];
 
 val keywords2 =
- ["and", "case", "do", "else", "end", "if", "in", "let", "local", "of",
+ Symset.make ["and", "case", "do", "else", "end", "if", "in", "let", "local", "of",
   "sig", "struct", "then", "while", "with"];
 
 val keywords3 =
- ["handle", "open", "raise"];
+ Symset.make ["handle", "open", "raise"];
 
 val lexicon = Scan.make_lexicon (map raw_explode keywords);
 
@@ -168,8 +168,8 @@
     val (markup, txt) =
       if not (is_keyword tok) then token_kind_markup kind
       else if is_delimiter tok then (Markup.ML_delimiter, "")
-      else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "")
-      else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "")
+      else if Symset.member keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "")
+      else if Symset.member keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "")
       else (Markup.ML_keyword1 |> Markup.keyword_properties, "");
   in ((pos, markup), txt) end;
 
@@ -196,8 +196,9 @@
 val scan_alphanumeric =
   Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) ::: scan_letdigs;
 
-val scan_symbolic =
-  Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
+val symbolic = Symset.make (raw_explode "!#$%&*+-/:<=>?@\\^`|~");
+
+val scan_symbolic = Scan.many1 (Symset.member symbolic o Symbol_Pos.symbol);
 
 in
 
@@ -244,8 +245,10 @@
 
 local
 
+val escape = Symset.make (raw_explode "\"\\abtnvfr");
+
 val scan_escape =
-  Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
+  Scan.one (Symset.member escape o Symbol_Pos.symbol) >> single ||
   $$$ "^" @@@
     (Scan.one (fn (s, _) => Char.ord #"@" <= ord s andalso ord s <= Char.ord #"_") >> single) ||
   Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --