diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index ddb9e777c9..21bc210d21 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -14,29 +14,35 @@ import Lean.Parser.Do namespace Lean namespace Parser +open Lean.PrettyPrinter +open Lean.PrettyPrinter.Parenthesizer +open Lean.PrettyPrinter.Formatter builtin_initialize - registerAlias "ws" checkWsBefore - registerAlias "noWs" checkNoWsBefore - registerAlias "linebreak" checkLinebreakBefore - 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 + register_parser_alias "ws" checkWsBefore + register_parser_alias "noWs" checkNoWsBefore + register_parser_alias "linebreak" checkLinebreakBefore + register_parser_alias "num" numLit + register_parser_alias "str" strLit + register_parser_alias "char" charLit + register_parser_alias "name" nameLit + register_parser_alias "ident" 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 "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 + registerAlias "notFollowedBy" (notFollowedBy · "element") - registerAlias "optional" optional - registerAlias "withPosition" withPosition - registerAlias "interpolatedStr" interpolatedStr - registerAlias "orelse" orelse - registerAlias "andthen" andthen - registerAlias "incQuotDepth" incQuotDepth + Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer + Formatter.registerAlias "notFollowedBy" notFollowedBy.formatter end Parser diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index d5aeee2098..52d76fd089 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -114,30 +114,4 @@ builtin_initialize 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 - -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 - end Lean diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index a15741c694..d0268f9329 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -456,20 +456,6 @@ instance : Coe Formatter FormatterAliasValue := { coe := AliasValue.const } instance : Coe (Formatter → Formatter) FormatterAliasValue := { coe := AliasValue.unary } instance : Coe (Formatter → Formatter → Formatter) FormatterAliasValue := { coe := AliasValue.binary } -builtin_initialize - registerAlias "ws" checkWsBefore.formatter - registerAlias "noWs" checkNoWsBefore.formatter - registerAlias "linebreak" checkLinebreakBefore.formatter - registerAlias "colGt" checkColGt.formatter - registerAlias "colGe" checkColGe.formatter - registerAlias "lookahead" lookahead.formatter - registerAlias "atomic" atomic.formatter - registerAlias "notFollowedBy" notFollowedBy.formatter - registerAlias "withPosition" withPosition.formatter - registerAlias "interpolatedStr" interpolatedStr.formatter - registerAlias "orelse" orelse.formatter - registerAlias "andthen" andthen.formatter - end Formatter open Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 6d6e76cf78..3b550bc38f 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -517,20 +517,6 @@ instance : Coe Parenthesizer ParenthesizerAliasValue := { coe := AliasValue.cons instance : Coe (Parenthesizer → Parenthesizer) ParenthesizerAliasValue := { coe := AliasValue.unary } instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) ParenthesizerAliasValue := { coe := AliasValue.binary } -builtin_initialize - registerAlias "ws" checkWsBefore.parenthesizer - registerAlias "noWs" checkNoWsBefore.parenthesizer - registerAlias "linebreak" checkLinebreakBefore.parenthesizer - registerAlias "colGt" checkColGt.parenthesizer - registerAlias "colGe" checkColGe.parenthesizer - registerAlias "lookahead" lookahead.parenthesizer - registerAlias "atomic" atomic.parenthesizer - registerAlias "notFollowedBy" notFollowedBy.parenthesizer - registerAlias "withPosition" withPosition.parenthesizer - registerAlias "interpolatedStr" interpolatedStr.parenthesizer - registerAlias "orelse" orelse.parenthesizer - registerAlias "andthen" andthen.parenthesizer - end Parenthesizer open Parenthesizer