From 1983c94fb9da6694661664b1ff673d47cf5bf837 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 12 Aug 2016 20:37:34 -0700
Subject: [PATCH] feat(emacs/lean-syntax): highlight mutual definitions, and
 attributes after definition keywords

---
 src/emacs/lean-syntax.el | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 1d327d634d..fab543ad52 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -127,6 +127,21 @@
   `((;; attributes
      (,(rx word-start "attribute" word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace))))
       (1 'font-lock-doc-face))
+     ;; attributes after definitions
+     (,(rx word-start
+           (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary"
+                      "hypothesis" "definition" "meta_definition" "constant" "meta_constant" "abbreviation"))
+           word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace)))
+           (zero-or-more whitespace)
+           (group (zero-or-more (not (any " \t\n\r{([")))))
+      (2 'font-lock-doc-face) (3 'font-lock-function-name-face))
+     ;; attribute after mutual_definitions
+     (,(rx word-start
+           (group (or "mutual_definition" "mutual_meta_definition" "mutual_inductive"))
+           word-end (zero-or-more whitespace) (group (one-or-more "[" (zero-or-more (not (any "]"))) "]" (zero-or-more whitespace)))
+           (zero-or-more whitespace)
+           (group (zero-or-more (not (any " \t\n\r{([,"))) (zero-or-more (zero-or-more whitespace) "," (zero-or-more whitespace) (not (any " \t\n\r{([,")))))
+      (2 'font-lock-doc-face) (3 'font-lock-function-name-face))
      ;; Constants which have a keyword as subterm
      (,(rx (or "∘if")) . 'font-lock-constant-face)
      ;; Keywords
@@ -142,14 +157,22 @@
      ;; ;; Constants
      (,lean-constants-regexp . 'font-lock-constant-face)
      (,lean-numerals-regexp . 'font-lock-constant-face)
-     ;; universe/inductive/theorem... "names"
+     ;; universe/inductive/theorem... "names" (without attributes)
      (,(rx word-start
            (group (or "inductive" "structure" "record" "theorem" "axiom" "axioms" "lemma" "proposition" "corollary"
                       "hypothesis" "definition" "meta_definition" "constant" "meta_constant" "abbreviation"))
            word-end
-           (zero-or-more (or whitespace "(" "{" "["))
+           (zero-or-more whitespace)
            (group (zero-or-more (not (any " \t\n\r{([")))))
       (2 'font-lock-function-name-face))
+     ;; meta_definitions "names" (without attributes)
+     (,(rx word-start
+           (group (or "mutual_definition" "mutual_meta_definition" "mutual_inductive"))
+           word-end
+           (zero-or-more whitespace)
+           (group (zero-or-more (not (any " \t\n\r{([,"))) (zero-or-more (zero-or-more whitespace) "," (zero-or-more whitespace) (not (any " \t\n\r{([,")))))
+      (2 'font-lock-function-name-face))
+
      ;; place holder
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; warnings