Summary: New indentation code using SMIE

* coq/coq.el (coq-build-prog-args): Avoid meaningless \- escape sequence.
(coq-use-smie): New custom var.
(coq-smie-grammar): New var.
(coq-smie-rules): New function.
(coq-guess-or-ask-for-string): Use use-region-p.
(coq-mode-config): Use smie-setup if available.
* lib/proof-compat.el (use-region-p): Provide fallback definition.

1 files changed, 10 insertions, 6 deletions

diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index a9fae654..3918b7ce 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -119,12 +119,12 @@ The value returned is the value of the last form in BODY."
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
-;;; A naughty hack to completion.el
-;;;
-;;; At the moment IMO completion too eagerly adds stuff to
-;;; its database: the completion-before-command function
-;;; makes every suffix be added as a completion!
+;;
+;; A naughty hack to completion.el
+;;
+;; At the moment IMO completion too eagerly adds stuff to
+;; its database: the completion-before-command function
+;; makes every suffix be added as a completion!
 
 (eval-after-load "completion"
 '(defun completion-before-command ()
@@ -137,6 +137,10 @@ The value returned is the value of the last form in BODY."
 ;;; Backward compatibility for Emacs 22
 ;;;
 
+(or (fboundp 'use-region-p)
+    (defun use-region-p ()
+      (and transient-mark-mode mark-active)))
+
 (or (fboundp 'characterp)
     (defun characterp (obj)
       (with-no-warnings (char-valid-p obj))))