diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index f9b269ec91..bea55d2dd4 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1100,6 +1100,7 @@ fun _ c s => def quotedSymbolFn {k : ParserKind} : ParserFn k := nodeFn `quotedSymbol (andthenFn (andthenFn (chFn '`') (rawFn (fun _ => takeUntilFn (fun c => c == '`')))) (chFn '`' true)) +-- TODO: remove after old frontend is gone def quotedSymbol {k : ParserKind} : Parser k := { fn := quotedSymbolFn } diff --git a/src/Init/Lean/Parser/Syntax.lean b/src/Init/Lean/Parser/Syntax.lean index cf9a50ffa4..88f628537b 100644 --- a/src/Init/Lean/Parser/Syntax.lean +++ b/src/Init/Lean/Parser/Syntax.lean @@ -54,11 +54,13 @@ def mixfixKind := «prefix» <|> «infix» <|> «infixl» <|> «infixr» <|> «p -- TODO delete reserve @[builtinCommandParser] def «reserve» := parser! "reserve " >> mixfixKind >> quotedSymbolPrec def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol -@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> mixfixSymbol >> darrow >> termParser +-- TODO: remove " := " after old frontend is gone +@[builtinCommandParser] def «mixfix» := parser! mixfixKind >> mixfixSymbol >> (" := " <|> darrow) >> termParser def strLitPrec := parser! strLit >> optPrecedence def identPrec := parser! ident >> optPrecedence -@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> darrow >> termParser +-- TODO: remove " := " after old frontend is gone +@[builtinCommandParser] def «notation» := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser @[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented" @[builtinCommandParser] def «syntax» := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident @[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident