fix(frontends/lean/decl_cmds): support local attribute with docstring (…

…#271) Fixes #270.
leanprover-community · May 25, 2020 · 61a8cb4 · 61a8cb4
1 parent d12975b
commit 61a8cb4
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 9 deletions.
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
@@ -346,10 +346,10 @@ environment open_export_cmd(parser & p, bool open) {
 static environment open_cmd(parser & p) { return open_export_cmd(p, true); }
 static environment export_cmd(parser & p) { return open_export_cmd(p, false); }
 
-static environment local_cmd(parser & p) {
+static environment local_cmd(parser & p, cmd_meta const & meta) {
     if (p.curr_is_token_or_id(get_attribute_tk())) {
         p.next();
-        return local_attribute_cmd(p);
+        return local_attribute_cmd(p, meta);
     } else {
         return local_notation_cmd(p);
     }

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
@@ -530,13 +530,13 @@ static environment modifiers_cmd(parser & p, cmd_meta const & _meta) {
     return p.env();
 }
 
-static environment attribute_cmd_core(parser & p, bool persistent) {
+static environment attribute_cmd_core(parser & p, bool persistent, cmd_meta const & meta) {
     buffer<name> ds;
     decl_attributes attributes(persistent);
     attributes.parse(p);
     // 'attribute [attr] definition ...'
     if (p.curr_is_command()) {
-        return modifiers_cmd(p, {attributes, {}, {}});
+        return modifiers_cmd(p, {attributes, meta.m_modifiers, meta.m_doc_string});
     }
     do {
         auto pos = p.pos();
@@ -553,12 +553,12 @@ static environment attribute_cmd_core(parser & p, bool persistent) {
     return env;
 }
 
-static environment attribute_cmd(parser & p) {
-    return attribute_cmd_core(p, true);
+static environment attribute_cmd(parser & p, cmd_meta const & meta) {
+    return attribute_cmd_core(p, true, meta);
 }
 
-environment local_attribute_cmd(parser & p) {
-    return attribute_cmd_core(p, false);
+environment local_attribute_cmd(parser & p, cmd_meta const & meta) {
+    return attribute_cmd_core(p, false, meta);
 }
 
 static environment compact_attribute_cmd(parser & p, cmd_meta const & meta) {

diff --git a/src/frontends/lean/decl_cmds.h b/src/frontends/lean/decl_cmds.h
@@ -23,7 +23,7 @@ bool parse_univ_params(parser & p, buffer<name> & ps);
 void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found_ls, parser const & p);
 
 /** \brief Parse a local attribute command */
-environment local_attribute_cmd(parser & p);
+environment local_attribute_cmd(parser & p, cmd_meta const & meta);
 void register_decl_cmds(cmd_table & r);
 
 void initialize_decl_cmds();

diff --git a/tests/lean/run/local_attr_doc.lean b/tests/lean/run/local_attr_doc.lean
@@ -0,0 +1,3 @@
+/-- `foo` is awesome -/
+local attribute [simp] -- command does not accept doc string
+def foo := false