max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: use register_parser_alias where possible

Browse source 
Fixes #494
This commit is contained in:
Sebastian Ullrich 2021-07-22 16:28:06 +02:00
parent 42e681a5a6
commit 5866e2bbb7
4 changed files with 26 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/Lean/Parser.lean
View file

@ -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

26
src/Lean/Parser/Extra.lean
View file

@ -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

14
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -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

14
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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