From 751f2d8b02ac19ec5d4889f353b950a1b92ec086 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 16 Aug 2016 13:54:08 -0400
Subject: [PATCH] refactor(frontends/lean): delegate all attribute parsing to
 `decl_attributes`

---
 src/frontends/lean/builtin_cmds.cpp  | 12 ++++++++++--
 src/frontends/lean/decl_attributes.h |  6 ++++--
 src/frontends/lean/notation_cmd.cpp  | 20 +++++++++++---------
 3 files changed, 25 insertions(+), 13 deletions(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 3f18a238ad..39b131bfe2 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -50,6 +50,7 @@ Author: Leonardo de Moura
 // #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parse_table.h"
+#include "frontends/lean/decl_attributes.h"
 
 namespace lean {
 environment section_cmd(parser & p) {
@@ -393,9 +394,16 @@ static environment register_simp_ext_cmd(parser & p) {
     environment env = p.env();
     name head = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected");
     name simp_ext_name = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected");
+
     unsigned prio = LEAN_DEFAULT_PRIORITY;
-    if (auto oprio = parse_priority(p))
-        prio = *oprio;
+    auto pos = p.pos();
+    decl_attributes attrs;
+    attrs.parse(p);
+    if (auto const & entry = head_opt(attrs.get_entries()))
+        throw parser_error(sstream() << "invalid #register_simp_ext_cmd command, unexpected attribute ["
+                                     << entry->m_attr->get_name() << "]", pos);
+    if (attrs.get_priority())
+        prio = *attrs.get_priority();
     bool persistent = true;
     env = add_simp_extension(env, p.ios(), head, simp_ext_name, prio, persistent);
     return env;
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index cdf2137dfe..27897a27a3 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -12,12 +12,12 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 class decl_attributes {
-private:
+public:
     struct entry {
         attribute const * m_attr;
         attr_data_ptr     m_params;
     };
-
+private:
     bool               m_persistent;
     bool               m_parsing_only;
     list<entry>        m_entries;
@@ -26,7 +26,9 @@ public:
     decl_attributes(bool persistent = true): m_persistent(persistent), m_parsing_only(false) {}
     void parse(parser & p);
     environment apply(environment env, io_state const & ios, name const & d) const;
+    list<entry> const & get_entries() const { return m_entries; }
     bool is_parsing_only() const { return m_parsing_only; }
+    optional<unsigned > get_priority() const { return m_prio; }
     operator bool() const { return static_cast<bool>(m_entries); }
 };
 }
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 2a9f1c3c1c..0b87fdc481 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/nested_declaration.h"
+#include "frontends/lean/decl_attributes.h"
 
 namespace lean {
 static std::string parse_symbol(parser & p, char const * msg) {
@@ -682,17 +683,18 @@ struct notation_modifiers {
     unsigned m_priority;
     notation_modifiers():m_parse_only(false), m_priority(LEAN_DEFAULT_NOTATION_PRIORITY) {}
     void parse(parser & p) {
-        while (true) {
-            if (p.curr_is_token(get_parsing_only_tk())) {
-                p.next();
-                p.check_token_next(get_rbracket_tk(), "invalid [parsing_only] attribute, ']' expected");
+        auto pos = p.pos();
+        decl_attributes attrs;
+        attrs.parse(p);
+        for (auto const & entry : attrs.get_entries()) {
+            if (entry.m_attr->get_name() == "parsing_only")
                 m_parse_only = true;
-            } else if (auto prio = parse_priority(p)) {
-                m_priority = *prio;
-            } else {
-                return;
-            }
+            else
+                throw parser_error(sstream() << "invalid notation: unexpected attribute ["
+                                             << entry.m_attr->get_name() << "]", pos);
         }
+        if (attrs.get_priority())
+            m_priority = *attrs.get_priority();
     }
 };