refactor: add Elab/Syntax.lean

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

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;

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