feat(src/frontends): order notation by priority in pretty-printer

src/frontends/lean/parser_config.cpp

@@ -202,9 +202,11 @@ transition read_transition(deserializer & d) {
     return transition(n, a, pp);
 }
 
+struct notation_prio_fn { unsigned operator()(notation_entry const & v) const { return v.priority(); } };
+
 struct notation_state {
     typedef rb_map<mpz, list<expr>, mpz_cmp_fn> num_map;
-    typedef head_map<notation_entry>            head_to_entries;
+    typedef head_map_prio<notation_entry, notation_prio_fn> head_to_entries;
     parse_table      m_nud;
     parse_table      m_led;
     num_map          m_num_map;

tests/lean/notation_pp_priority.lean

@@ -0,0 +1,28 @@
+prelude
+
+import init.data.nat.basic
+
+noncomputable theory
+
+constant some_type : Type
+constants foo bar : some_type
+
+/-
+  Test that notation with a high priority is used by the pretty-printer,
+  regardless of the order in which they are declared.
+-/
+section
+  notation [priority 2000] `high_before_low` := foo
+  notation [priority 1] `low_after_high` := foo
+
+  def test_high_before_low := foo
+  #print test_high_before_low
+end
+
+section
+  notation [priority 1] `low_before_high` := bar
+  notation [priority 2000] `high_after_low` := bar
+
+  def test_high_after_low := bar
+  #print test_high_after_low
+end

tests/lean/notation_pp_priority.lean.expected.out

@@ -0,0 +1,4 @@
+noncomputable def test_high_before_low : some_type :=
+high_before_low
+noncomputable def test_high_after_low : some_type :=
+high_after_low