From 2d83d49341e19c999965fbfa73037a2f65869062 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Jan 2020 14:22:55 -0800
Subject: [PATCH] refactor: add `Elab/Syntax.lean`

---
 src/Init/Lean/Elab.lean         |  1 +
 src/Init/Lean/Elab/Command.lean | 13 -------------
 src/Init/Lean/Elab/Syntax.lean  | 28 ++++++++++++++++++++++++++++
 3 files changed, 29 insertions(+), 13 deletions(-)
 create mode 100644 src/Init/Lean/Elab/Syntax.lean

diff --git a/src/Init/Lean/Elab.lean b/src/Init/Lean/Elab.lean
index 3bb2e15a56..475f45fb64 100644
--- a/src/Init/Lean/Elab.lean
+++ b/src/Init/Lean/Elab.lean
@@ -16,3 +16,4 @@ import Init.Lean.Elab.Frontend
 import Init.Lean.Elab.BuiltinNotation
 import Init.Lean.Elab.Declaration
 import Init.Lean.Elab.Tactic
+import Init.Lean.Elab.Syntax
diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 45ecbb1a3d..69af6577cf 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -570,19 +570,6 @@ fun stx => do
   | Syntax.atom _ "false" => setOption ref optionName (DataValue.ofBool false)
   | _ => logError val ("unexpected set_option value " ++ toString val)
 
-@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
-fun stx => do
-  let catName  := stx.getIdAt 1;
-  let attrName := catName.appendAfter "Parser";
-  env ← getEnv;
-  env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
-  setEnv env
-
-
-@[builtinCommandElab syntax] def elabSyntax : CommandElab :=
-fun stx =>
-  throwError stx ("not implemented yet " ++ toString stx)
-
 @[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
 -- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
 let id             := declId.getIdAt 0;
diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
new file mode 100644
index 0000000000..d793e67d60
--- /dev/null
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Lean.Elab.Command
+
+namespace Lean
+namespace Elab
+namespace Command
+
+@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
+fun stx => do
+  let catName  := stx.getIdAt 1;
+  let attrName := catName.appendAfter "Parser";
+  env ← getEnv;
+  env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
+  setEnv env
+
+
+@[builtinCommandElab syntax] def elabSyntax : CommandElab :=
+fun stx =>
+  throwError stx ("not implemented yet " ++ toString stx)
+
+end Command
+end Elab
+end Lean