From 2b1869790c751e6d2f154482856812fa5bf12e28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jan 2020 13:00:19 -0800
Subject: [PATCH] feat: add tactic parser attributes

---
 src/Init/Lean/Parser.lean        |  1 +
 src/Init/Lean/Parser/Tactic.lean | 33 ++++++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 src/Init/Lean/Parser/Tactic.lean

diff --git a/src/Init/Lean/Parser.lean b/src/Init/Lean/Parser.lean
index a1ef5626bc..ac0a61b6c8 100644
--- a/src/Init/Lean/Parser.lean
+++ b/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
diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
new file mode 100644
index 0000000000..bbad3776a7
--- /dev/null
+++ b/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