chore: symbolOrIdent ==> nonReservedSymbol

src/Init/Lean/Parser/Command.lean

@@ -86,7 +86,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def exit           := parser! "#exit"
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
-@[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (symbolOrIdent "true" <|> symbolOrIdent "false" <|> strLit <|> numLit)
+@[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
 @[builtinCommandParser] def «attribute»    := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident
 @[builtinCommandParser] def «export»       := parser! "export " >> ident >> "(" >> many1 ident >> ")"
 def openHiding       := parser! try (ident >> "hiding") >> many1 ident
@@ -98,7 +98,7 @@ def openSimple       := parser! many1 ident
 @[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
 
 /- Lean3 command declaration commands -/
-def maxPrec := parser! symbolOrIdent "max"
+def maxPrec := parser! nonReservedSymbol "max"
 def precedenceLit : Parser := numLit <|> maxPrec
 def «precedence» := parser! " : " >> precedenceLit
 def quotedSymbolPrec := parser! quotedSymbol >> optional «precedence»

src/Init/Lean/Parser/Level.lean

@@ -21,8 +21,8 @@ categoryParser `level rbp
 namespace Level
 
 @[builtinLevelParser] def paren  := parser! symbol "(" appPrec >> levelParser >> ")"
-@[builtinLevelParser] def max    := parser! symbolOrIdent "max"  >> many1 (levelParser appPrec)
-@[builtinLevelParser] def imax   := parser! symbolOrIdent "imax" >> many1 (levelParser appPrec)
+@[builtinLevelParser] def max    := parser! nonReservedSymbol "max "  >> many1 (levelParser appPrec)
+@[builtinLevelParser] def imax   := parser! "imax" >> many1 (levelParser appPrec)
 @[builtinLevelParser] def hole   := parser! "_"
 @[builtinLevelParser] def num    := parser! numLit
 @[builtinLevelParser] def ident  := parser! ident

src/Init/Lean/Parser/Parser.lean

@@ -897,7 +897,7 @@ symbolAux sym lbp
     For example, the universe `max` Function is parsed using this combinator so that
     it can still be used as an identifier outside of universes (but registering it
     as a token in a Term Syntax would not break the universe Parser). -/
-def symbolOrIdentFnAux (sym : String) (errorMsg : String) : BasicParserFn :=
+def nonReservedSymbolFnAux (sym : String) (errorMsg : String) : BasicParserFn :=
 fun c s =>
   let startPos := s.pos;
   let s := tokenFn c s;
@@ -914,16 +914,16 @@ fun c s =>
         s.mkErrorAt errorMsg startPos
     | _ => s.mkErrorAt errorMsg startPos
 
-@[inline] def symbolOrIdentFn (sym : String) : BasicParserFn :=
-symbolOrIdentFnAux sym ("'" ++ sym ++ "'")
+@[inline] def nonReservedSymbolFn (sym : String) : BasicParserFn :=
+nonReservedSymbolFnAux sym ("'" ++ sym ++ "'")
 
-def symbolOrIdentInfo (sym : String) : ParserInfo :=
+def nonReservedSymbolInfo (sym : String) : ParserInfo :=
 { firstTokens  := FirstTokens.tokens [ { val := sym }, { val := "ident" } ] }
 
-@[inline] def symbolOrIdent {k : ParserKind} (sym : String) : Parser k :=
+@[inline] def nonReservedSymbol {k : ParserKind} (sym : String) : Parser k :=
 let sym := sym.trim;
-{ info := symbolOrIdentInfo sym,
-  fn   := fun _ => symbolOrIdentFn sym }
+{ info := nonReservedSymbolInfo sym,
+  fn   := fun _ => nonReservedSymbolFn sym }
 
 partial def strAux (sym : String) (errorMsg : String) : Nat → BasicParserFn
 | j, c, s =>