diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 8870b26c74..6d8121c504 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -26,21 +26,21 @@ builtin_initialize register_parser_alias "str" strLit register_parser_alias "char" charLit register_parser_alias "name" nameLit - register_parser_alias "ident" ident + register_parser_alias ident register_parser_alias "colGt" checkColGt register_parser_alias "colGe" checkColGe - register_parser_alias "lookahead" lookahead - register_parser_alias "atomic" atomic - register_parser_alias "many" many - register_parser_alias "many1" many1 - register_parser_alias "manyIndent" manyIndent - register_parser_alias "many1Indent" many1Indent - register_parser_alias "optional" optional - register_parser_alias "withPosition" withPosition - register_parser_alias "interpolatedStr" interpolatedStr - register_parser_alias "orelse" orelse - register_parser_alias "andthen" andthen - register_parser_alias "incQuotDepth" incQuotDepth + register_parser_alias lookahead + register_parser_alias atomic + register_parser_alias many + register_parser_alias many1 + register_parser_alias manyIndent + register_parser_alias many1Indent + register_parser_alias optional + register_parser_alias withPosition + register_parser_alias interpolatedStr + register_parser_alias orelse + register_parser_alias andthen + register_parser_alias incQuotDepth registerAlias "notFollowedBy" (notFollowedBy · "element") Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 4f4255f2c4..43b6e3b248 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -116,11 +116,11 @@ def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple builtin_initialize register_parser_alias "declModifiers" declModifiersF register_parser_alias "nestedDeclModifiers" declModifiersT - register_parser_alias "declId" declId - register_parser_alias "declSig" declSig - register_parser_alias "declVal" declVal - register_parser_alias "optDeclSig" optDeclSig - register_parser_alias "openDecl" openDecl + register_parser_alias declId + register_parser_alias declSig + register_parser_alias declVal + register_parser_alias optDeclSig + register_parser_alias openDecl end Command diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index d674790317..94c60efe31 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -28,8 +28,8 @@ def termBeforeDo := withForbidden "do" termParser attribute [runBuiltinParserAttributeHooks] doSeq termBeforeDo builtin_initialize - register_parser_alias "doSeq" doSeq - register_parser_alias "termBeforeDo" termBeforeDo + register_parser_alias doSeq + register_parser_alias termBeforeDo def notFollowedByRedefinedTermToken := -- Remark: we don't currently support `open` and `set_option` in `do`-blocks, but we include them in the following list to fix the ambiguity diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 52d76fd089..af88d44163 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -98,19 +98,20 @@ namespace Parser attribute [runBuiltinParserAttributeHooks] ppHardSpace ppSpace ppLine ppGroup ppIndent ppDedent -macro "register_parser_alias" aliasName:strLit declName:ident : term => +macro "register_parser_alias" aliasName?:optional(strLit) declName:ident : term => + let aliasName := aliasName?.getD (Syntax.mkStrLit declName.getId.toString) `(do Parser.registerAlias $aliasName $declName PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter)) PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer))) builtin_initialize - register_parser_alias "group" group - register_parser_alias "ppHardSpace" ppHardSpace - register_parser_alias "ppSpace" ppSpace - register_parser_alias "ppLine" ppLine - register_parser_alias "ppGroup" ppGroup - register_parser_alias "ppIndent" ppIndent - register_parser_alias "ppDedent" ppDedent + register_parser_alias group + register_parser_alias ppHardSpace + register_parser_alias ppSpace + register_parser_alias ppLine + register_parser_alias ppGroup + register_parser_alias ppIndent + register_parser_alias ppDedent end Parser diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 531dfb6b22..339eb4d78a 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -10,7 +10,7 @@ namespace Parser namespace Tactic builtin_initialize - register_parser_alias "tacticSeq" tacticSeq + register_parser_alias tacticSeq @[builtinTacticParser] def «unknown» := leading_parser withPosition (ident >> errorAtSavedPos "unknown tactic" true) @[builtinTacticParser] def nestedTactic := tacticSeqBracketed diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 64eef68dd3..163275cf91 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -269,16 +269,17 @@ end Term @[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> incQuotDepth levelParser >> ")" +open Term in builtin_initialize - register_parser_alias "letDecl" Term.letDecl - register_parser_alias "haveDecl" Term.haveDecl - register_parser_alias "sufficesDecl" Term.sufficesDecl - register_parser_alias "letRecDecls" Term.letRecDecls - register_parser_alias "hole" Term.hole - register_parser_alias "syntheticHole" Term.syntheticHole - register_parser_alias "matchDiscr" Term.matchDiscr - register_parser_alias "bracketedBinder" Term.bracketedBinder - register_parser_alias "attrKind" Term.attrKind + register_parser_alias letDecl + register_parser_alias haveDecl + register_parser_alias sufficesDecl + register_parser_alias letRecDecls + register_parser_alias hole + register_parser_alias syntheticHole + register_parser_alias matchDiscr + register_parser_alias bracketedBinder + register_parser_alias attrKind end Parser end Lean