feat: add tactic parser attributes

src/Init/Lean/Parser.lean

@@ -7,5 +7,6 @@ prelude
 import Init.Lean.Parser.Parser
 import Init.Lean.Parser.Level
 import Init.Lean.Parser.Term
+import Init.Lean.Parser.Tactic
 import Init.Lean.Parser.Command
 import Init.Lean.Parser.Module

src/Init/Lean/Parser/Tactic.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import Init.Lean.Parser.Term
+
+namespace Lean
+namespace Parser
+
+@[init] def regBuiltinTacticParserAttr : IO Unit :=
+registerBuiltinParserAttribute `builtinTacticParser `tactic
+
+@[init] def regTacticParserAttribute : IO Unit :=
+registerBuiltinDynamicParserAttribute `tacticParser `tactic
+
+@[inline] def tacticParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
+categoryParser `tactic rbp
+
+namespace Tactic
+
+
+end Tactic
+
+namespace Term
+
+@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> tacticParser >> "end"
+
+end Term
+
+end Parser
+end Lean