feat(library/init/lean/parser/command): add declaration draft

library/init/lean/parser/command.lean

@@ -37,14 +37,26 @@ def «noncomputable»  := parser! "noncomputable"
 def «unsafe»         := parser! "unsafe"
 def declModifiers    := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe»
 def declId           := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
-def declSig          := parser! many1 Term.bracktedBinder >> Term.typeSpec
-def optDeclSig       := parser! many1 Term.bracktedBinder >> Term.optType
+def declSig          := parser! many Term.bracktedBinder >> Term.typeSpec
+def optDeclSig       := parser! many Term.bracktedBinder >> Term.optType
 def declValSimple    := parser! " := " >> termParser
 def declValEqns      := parser! many1Indent Term.equation "equations must be indented"
 def declVal          := declValSimple <|> declValEqns
 def «def»            := parser! "def " >> declId >> optDeclSig >> declVal
 def «theorem»        := parser! "theorem " >> declId >> declSig >> declVal
 
+def declaration      := declModifiers >> («def» <|> «theorem»)
+
+/- TODO: remove this hack by improving how we compute `Parser.info.firstTokens` -/
+def declTokens := ["/--", "@[", "private", "protected", "noncomputable", "unsafe", "def", "theorem"]
+
+@[builtinCommandParser] def declEntry : Parser :=
+{ info := {
+    firstTokens := FirstTokens.tokens $ declTokens.map $ fun tk => { val := tk },
+    .. declaration.info
+  },
+  fn   := declaration.fn }
+
 end Command
 
 end Parser

tests/playground/cmdparsertest1.lean

@@ -0,0 +1,24 @@
+import init.lean.parser.command
+open Lean
+open Lean.Parser
+
+def testParser (input : String) : IO Unit :=
+do
+env ← mkEmptyEnvironment;
+cmdPTables ← builtinCommandParsingTable.get;
+stx ← IO.ofExcept $ runParser env cmdPTables input "<input>" "command";
+IO.println stx
+
+def test (is : List String) : IO Unit :=
+is.mfor $ fun input => do
+  IO.println input;
+  testParser input
+
+def main (xs : List String) : IO Unit :=
+do
+test [
+"@[inline] def x := 2",
+"protected def length.{u} {α : Type u} : List α → Nat
+  | [] := 0
+  | (a::as) := 1 + length as"
+]