src/Pure/Isar/token.scala

       val cmt = comment ^^ (x => Token(Token.Kind.COMMENT, x))
 
       string | (alt_string | (verb | (cart | cmt)))
     }
 
-    private def other_token(minor: Scan.Lexicon, major: Scan.Lexicon): Parser[Token] =
+    private def other_token(keywords: Keyword.Keywords): Parser[Token] =
     {
       val letdigs1 = many1(Symbol.is_letdig)
       val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>")
       val id =
         one(Symbol.is_letter) ~

       val sym_ident =
         (many1(Symbol.is_symbolic_char) | one(sym => Symbol.is_symbolic(sym))) ^^
         (x => Token(Token.Kind.SYM_IDENT, x))
 
       val keyword =
-        literal(minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) |||
-        literal(major) ^^ (x => Token(Token.Kind.COMMAND, x))
+        literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) |||
+        literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x))
 
       val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
 
       val recover_delimited =
         (recover_quoted("\"") |

       space | (recover_delimited |
         (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
           keyword) | bad))
     }
 
-    def token(minor: Scan.Lexicon, major: Scan.Lexicon): Parser[Token] =
-      delimited_token | other_token(minor, major)
-
-    def token_line(minor: Scan.Lexicon, major: Scan.Lexicon, ctxt: Scan.Line_Context)
+    def token(keywords: Keyword.Keywords): Parser[Token] =
+      delimited_token | other_token(keywords)
+
+    def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context)
       : Parser[(Token, Scan.Line_Context)] =
     {
       val string =
         quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) }
       val alt_string =
         quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) }
       val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) }
       val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) }
       val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) }
-      val other = other_token(minor, major) ^^ { case x => (x, Scan.Finished) }
+      val other = other_token(keywords) ^^ { case x => (x, Scan.Finished) }
 
       string | (alt_string | (verb | (cart | (cmt | other))))
     }
   }