diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index 1b57e2a7d8..7e0e1bc2df 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -13,6 +13,35 @@ import Lean.Parser.Syntax import Lean.Parser.Do namespace Lean +namespace Parser + +builtin_initialize + registerAlias "ws" checkWsBefore + registerAlias "noWs" checkNoWsBefore + registerAlias "num" numLit + registerAlias "str" strLit + registerAlias "char" charLit + registerAlias "name" nameLit + registerAlias "ident" ident + registerAlias "colGt" checkColGt + registerAlias "colGe" checkColGe + registerAlias "lookahead" lookahead + registerAlias "atomic" atomic + registerAlias "many" many + registerAlias "many1" many1 + registerAlias "notFollowedBy" (notFollowedBy · "element") + registerAlias "optional" optional + registerAlias "withPosition" withPosition + registerAlias "interpolatedStr" interpolatedStr + registerAlias "sepBy" sepBy + registerAlias "sepBy1" sepBy1 + registerAlias "orelse" orelse + registerAlias "andthen" andthen + registerAlias "sepByT" (sepBy (allowTrailingSep := true)) + registerAlias "sepBy1T" (sepBy1 (allowTrailingSep := true)) + +end Parser + namespace PrettyPrinter namespace Parenthesizer diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 1e8d44fca2..25bab18c28 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -268,31 +268,6 @@ def ensureBinaryParserAlias (aliasName : Name) : IO Unit := def ensureConstantParserAlias (aliasName : Name) : IO Unit := discard $ getConstAlias parserAliasesRef aliasName -builtin_initialize - registerAlias "ws" checkWsBefore - registerAlias "noWs" checkNoWsBefore - registerAlias "num" numLit - registerAlias "str" strLit - registerAlias "char" charLit - registerAlias "name" nameLit - registerAlias "ident" ident - registerAlias "colGt" checkColGt - registerAlias "colGe" checkColGe - registerAlias "lookahead" lookahead - registerAlias "atomic" atomic - registerAlias "many" many - registerAlias "many1" many1 - registerAlias "notFollowedBy" (notFollowedBy · "element") - registerAlias "optional" optional - registerAlias "withPosition" withPosition - registerAlias "interpolatedStr" interpolatedStr - registerAlias "sepBy" sepBy - registerAlias "sepBy1" sepBy1 - registerAlias "orelse" orelse - registerAlias "andthen" andthen - registerAlias "sepByT" (sepBy (allowTrailingSep := true)) - registerAlias "sepBy1T" (sepBy1 (allowTrailingSep := true)) - partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser := let rec visit : ParserDescr → ImportM Parser | ParserDescr.const n => getConstAlias parserAliasesRef n diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 38d99c19a6..2d053f4e45 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -82,4 +82,39 @@ builtin_initialize registerParserAlias! "ppDedent" ppDedent end Parser + +open Parser + +open PrettyPrinter.Parenthesizer (registerAlias) in +builtin_initialize + registerAlias "num" numLit.parenthesizer + registerAlias "scientific" scientificLit.parenthesizer + registerAlias "str" strLit.parenthesizer + registerAlias "char" charLit.parenthesizer + registerAlias "name" nameLit.parenthesizer + registerAlias "ident" ident.parenthesizer + registerAlias "many" many.parenthesizer + registerAlias "many1" many1.parenthesizer + registerAlias "optional" optional.parenthesizer + registerAlias "sepBy" sepBy.parenthesizer + registerAlias "sepBy1" sepBy1.parenthesizer + registerAlias "sepByT" sepBy.parenthesizer + registerAlias "sepBy1T" sepBy1.parenthesizer + +open PrettyPrinter.Formatter (registerAlias) in +builtin_initialize + registerAlias "num" numLit.formatter + registerAlias "scientific" scientificLit.formatter + registerAlias "str" strLit.formatter + registerAlias "char" charLit.formatter + registerAlias "name" nameLit.formatter + registerAlias "ident" ident.formatter + registerAlias "many" many.formatter + registerAlias "many1" many1.formatter + registerAlias "optional" optional.formatter + registerAlias "sepBy" sepBy.formatter + registerAlias "sepBy1" sepBy1.formatter + registerAlias "sepByT" sepBy.formatter + registerAlias "sepBy1T" sepBy1.formatter + end Lean diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index a4fa6a9f59..228e4428ad 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -445,28 +445,15 @@ instance : Coe (Formatter → Formatter → Formatter) FormatterAliasValue := { builtin_initialize registerAlias "ws" checkWsBefore.formatter registerAlias "noWs" checkNoWsBefore.formatter - registerAlias "num" (withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.formatter) - registerAlias "scientific" (withAntiquot.formatter (mkAntiquot.formatter' "scientificLit" `scientificLit) scientificLitNoAntiquot.formatter) - registerAlias "str" (withAntiquot.formatter (mkAntiquot.formatter' "strLit" `strLit) strLitNoAntiquot.formatter) - registerAlias "char" (withAntiquot.formatter (mkAntiquot.formatter' "charLit" `charLit) charLitNoAntiquot.formatter) - registerAlias "name" (withAntiquot.formatter (mkAntiquot.formatter' "nameLit" `nameLit) nameLitNoAntiquot.formatter) - registerAlias "ident" (withAntiquot.formatter (mkAntiquot.formatter' "ident" `ident) identNoAntiquot.formatter) registerAlias "colGt" checkColGt.formatter registerAlias "colGe" checkColGe.formatter registerAlias "lookahead" lookahead.formatter registerAlias "atomic" atomic.formatter - registerAlias "many" many.formatter - registerAlias "many1" many1.formatter registerAlias "notFollowedBy" notFollowedBy.formatter - registerAlias "optional" optional.formatter registerAlias "withPosition" withPosition.formatter registerAlias "interpolatedStr" interpolatedStr.formatter - registerAlias "sepBy" sepBy.formatter - registerAlias "sepBy1" sepBy1.formatter registerAlias "orelse" orelse.formatter registerAlias "andthen" andthen.formatter - registerAlias "sepByT" sepBy.formatter - registerAlias "sepBy1T" sepBy1.formatter @[export lean_pretty_printer_formatter_interpret_parser_descr] unsafe def interpretParserDescr : ParserDescr → CoreM Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 38ae5e7805..23025f8635 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -500,28 +500,15 @@ instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) Parenthesizer builtin_initialize registerAlias "ws" checkWsBefore.parenthesizer registerAlias "noWs" checkNoWsBefore.parenthesizer - registerAlias "num" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer) - registerAlias "scientific" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "scientificLit" `scientificLit) scientificLitNoAntiquot.parenthesizer) - registerAlias "str" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer) - registerAlias "char" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer) - registerAlias "name" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer) - registerAlias "ident" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer) registerAlias "colGt" checkColGt.parenthesizer registerAlias "colGe" checkColGe.parenthesizer registerAlias "lookahead" lookahead.parenthesizer registerAlias "atomic" atomic.parenthesizer - registerAlias "many" many.parenthesizer - registerAlias "many1" many1.parenthesizer registerAlias "notFollowedBy" notFollowedBy.parenthesizer - registerAlias "optional" optional.parenthesizer registerAlias "withPosition" withPosition.parenthesizer registerAlias "interpolatedStr" interpolatedStr.parenthesizer - registerAlias "sepBy" sepBy.parenthesizer - registerAlias "sepBy1" sepBy1.parenthesizer registerAlias "orelse" orelse.parenthesizer registerAlias "andthen" andthen.parenthesizer - registerAlias "sepByT" sepBy.parenthesizer - registerAlias "sepBy1T" sepBy1.parenthesizer @[export lean_pretty_printer_parenthesizer_interpret_parser_descr] unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer