From 95ffdca3f7ca40683a6f4daf6039e13f42d947ee Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 1 Oct 2016 13:27:08 -0700
Subject: [PATCH] feat(frontends/lean/decl_attributes): add 'default_priority'
 attribute

---
 src/frontends/lean/decl_attributes.cpp | 20 +++++++++++++++++++-
 src/frontends/lean/decl_attributes.h   |  3 +++
 src/frontends/lean/init_module.cpp     |  3 +++
 3 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index 69a4e8885d..89bfdf387f 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/sexpr/option_declarations.h"
 #include "library/attribute_manager.h"
 #include "library/constants.h"
 #include "library/normalize.h"
@@ -15,6 +16,15 @@ Author: Leonardo de Moura
 #include "frontends/lean/util.h"
 
 namespace lean {
+// ==========================================
+// configuration options
+static name * g_default_priority = nullptr;
+
+unsigned get_default_priority(options const & opts) {
+    return opts.get_unsigned(*g_default_priority, LEAN_DEFAULT_PRIORITY);
+}
+// ==========================================
+
 void decl_attributes::parse_core(parser & p, bool compact) {
     while (true) {
         auto pos = p.pos();
@@ -111,7 +121,7 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
                                           << "]: no prior declaration on " << d);
             env = entry.m_attr->unset(env, ios, d, m_persistent);
         } else {
-            unsigned prio = m_prio ? *m_prio : LEAN_DEFAULT_PRIORITY;
+            unsigned prio = m_prio ? *m_prio : get_default_priority(ios.get_options());
             env = entry.m_attr->set_untyped(env, ios, d, prio, entry.m_params, m_persistent);
         }
     }
@@ -132,4 +142,12 @@ bool decl_attributes::has_class() const {
     return false;
 }
 
+void initialize_decl_attributes() {
+    g_default_priority = new name{"default_priority"};
+    register_unsigned_option(*g_default_priority, LEAN_DEFAULT_PRIORITY, "default priority for attributes");
+}
+
+void finalize_decl_attributes() {
+    delete g_default_priority;
+}
 }
diff --git a/src/frontends/lean/decl_attributes.h b/src/frontends/lean/decl_attributes.h
index a771811945..281abb4b32 100644
--- a/src/frontends/lean/decl_attributes.h
+++ b/src/frontends/lean/decl_attributes.h
@@ -39,4 +39,7 @@ public:
     bool has_class() const;
     operator bool() const { return static_cast<bool>(m_entries); }
 };
+
+void initialize_decl_attributes();
+void finalize_decl_attributes();
 }
diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp
index 1b0f90dc24..fad1e8a73c 100644
--- a/src/frontends/lean/init_module.cpp
+++ b/src/frontends/lean/init_module.cpp
@@ -24,9 +24,11 @@ Author: Leonardo de Moura
 #include "frontends/lean/match_expr.h"
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/tactic_notation.h"
+#include "frontends/lean/decl_attributes.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
+    initialize_decl_attributes();
     initialize_prenum();
     initialize_tokens();
     initialize_token_table();
@@ -69,5 +71,6 @@ void finalize_frontend_lean_module() {
     finalize_token_table();
     finalize_tokens();
     finalize_prenum();
+    finalize_decl_attributes();
 }
 }