Fixing compilation. Still need to verify some smie stuff on different versions of emacs.

2 files changed, 25 insertions, 21 deletions

diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el
index a87beb82..c40adda8 100644
--- a/coq/coq-smie-lexer.el
+++ b/coq/coq-smie-lexer.el
@@ -14,20 +14,23 @@
 ;; - We identify the different types of bullets (First approximation).
 ;; - We distinguish "with match" from other "with".
 
-(setq coq-smie-dot-friends '("*." "-*." "|-*." "*|-*."))
+(require 'coq-indent)
+(require 'smie)
+
+(defconst coq-smie-dot-friends '("*." "-*." "|-*." "*|-*."))
 
 ; for debuging
 (defun coq-time-indent ()
   (interactive)
-  (let ((deb (time-to-seconds)))
+  (let ((deb (float-time)))
     (smie-indent-line)
-    (message "time: %S"(- (time-to-seconds) deb))))
+    (message "time: %S"(- (float-time) deb))))
 
 (defun coq-time-indent-region (beg end)
   (interactive "r")
-  (let ((deb (time-to-seconds)))
+  (let ((deb (float-time)))
     (indent-region beg end nil)
-    (message "time: %S"(- (time-to-seconds) deb))))
+    (message "time: %S"(- (float-time) deb))))
 
 
 
@@ -131,9 +134,9 @@ command (and inside parenthesis)."
 			 (coq-smie-search-token-forward
 			  (append parops (cons "." nil))
 			  end ignore-between)
-			 (cons "." nil))) ;coq-smie-dot-friends
+			 (cons "." nil)) ;coq-smie-dot-friends
 		  (goto-char (point))
-		  next)
+		  next))
 	      ;; Do not consider "." when not followed by a space
 	      (when (or (not (equal next "."))
 			(looking-at "[[:space:]]"))
@@ -656,18 +659,19 @@ Lemma foo: forall n,
 ; To show the bug. Comment this and then try to indent the following:
 ; Module X.
 ; Module Y. <-- here -->  Error: (wrong-type-argument integer-or-marker-p nil)
-(defun smie-indent--parent ()
-  (or smie--parent
-      (save-excursion
-	(let* ((pos (point))
-	       (tok (funcall smie-forward-token-function)))
-	  (unless (numberp (cadr (assoc tok smie-grammar)))
-	    (goto-char pos))
-	  (setq smie--parent
-		(or (smie-backward-sexp 'halfsexp)
-		    (let (res)
-		      (while (null (setq res (smie-backward-sexp))))
-		      (list nil (point) (nth 2 res)))))))))
+; No need anymore?
+;; (defun smie-indent--parent ()
+;;   (or smie--parent
+;;       (save-excursion
+;; 	(let* ((pos (point))
+;; 	       (tok (funcall smie-forward-token-function)))
+;; 	  (unless (numberp (cadr (assoc tok smie-grammar)))
+;; 	    (goto-char pos))
+;; 	  (setq smie--parent
+;; 		(or (smie-backward-sexp 'halfsexp)
+;; 		    (let (res)
+;; 		      (while (null (setq res (smie-backward-sexp))))
+;; 		      (list nil (point) (nth 2 res)))))))))
 
 (defun coq-smie-rules (kind token)
   "Indentation rules for Coq.  See `smie-rules-function'.
@@ -775,4 +779,4 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
 
 
 
-(provide 'coq-smie-lexer)
\ No newline at end of file
+(provide 'coq-smie-lexer)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 2030d141..5d80c114 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -328,7 +328,7 @@
   "Coq tactic(al)s that solve a subgoal."
   )
 
-(setq develock-coq-font-lock-keywords
+(defvar develock-coq-font-lock-keywords
   '((develock-find-long-lines
      (1 'develock-long-line-1 t)
      (2 'develock-long-line-2 t))