Making non recursive functions to make fsf emacs happy, not yet finished.

3 files changed, 124 insertions, 105 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index da75f8d0..2bf3b9b9 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -21,33 +21,40 @@
 	  (lgthrest (max-length-db (cdr l))))
       (max lgth lgthrest))))
 
+; this make emacs accept recursive versiond of these functions 
+;(setq max-lisp-eval-depth 10000)
+;(setq max-specpdl-size 30000)
+
+(defun coq-build-menu-from-db-internal (db lgth menuwidth)
+  "Take a keyword database DB and return insertion menus for them."
+  (let ((l db) (res ()) (size lgth)
+	(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
+    (while (and l (> size 0))
+      (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
+	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
+	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
+	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion 
+	     (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
+	     (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
+	     (e6 (car-safe tl5))	; e6 = function for smart insertion
+	     (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu 
+	     (entry-with (max (- menuwidth (length e1)) 0))
+	     (spaces (make-string entry-with ? ))
+	     ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth))
+	     )
+	(when (not e7)			; if not hidden
+	  (let ((menu-entry 
+		 (vector 
+		  ;; menu entry label
+		  (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")")))
+		   ;;insertion function if present otherwise insert completion
+		   (if e6 e6 `(holes-insert-and-expand ,e3))
+		   t)))
+	    (setq res (nconc res (list menu-entry)))));; append *in place*
+	(setq l tl)
+	(setq size (- size 1))))
+    res))
 
-(defun coq-build-menu-from-db-internal (l size menuwidth)
-  "Take a keyword database L and return insertion menus for them."
-  (when (and l (> size 0))
-    (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
-	   (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-	   (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-	   (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion 
-	   (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-	   (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-	   (e6 (car-safe tl5))		; e6 = function for smart insertion
-	   (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu 
-	   (entry-with (max (- menuwidth (length e1)) 0))
-	   (spaces (make-string entry-with ? ))
-	   (restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)))
-      (if (not e7)			; if not hidden
-	  (cons 
-	   (vector 
-	    (concat e1
-		    (if (not e2) ""
-		      (concat spaces "("  e2
-			      (substitute-command-keys " \\[expand-abbrev]") ")")))
-	    (if e6 e6			; insertion function if present
-	      `(holes-insert-and-expand ,e3)) ; otherwise insert completion
-	    t)
-	   restofmenu)
-	restofmenu))))
 
 (defun coq-build-title-menu (l size)
     (concat (car-safe (car-safe l))
@@ -55,48 +62,52 @@
 	  (car-safe (car-safe (nthcdr (- size 1) l)))))
 
 
-(defun coq-build-menu-from-db (l &optional size)
-  "Take a keyword database L and return a list of insertion menus for
+(defun coq-build-menu-from-db (db &optional size)
+  "Take a keyword database DB and return a list of insertion menus for
  them.
 Submenus contain SIZE entries (default 30)."
-  (let ((lgth (length l)) (sz (or size 30)) (wdth (+ 2 (max-length-db coq-tactics-db))))
-    (when l
-      (if (<= lgth sz) 
-	  (cons (cons (coq-build-title-menu l lgth)
-		      (coq-build-menu-from-db-internal l lgth wdth)) nil)
-	(cons (cons (coq-build-title-menu l sz)
-		    (coq-build-menu-from-db-internal l sz wdth))
-	      (coq-build-menu-from-db (nthcdr sz l) sz))))))
-
-
-(defun coq-build-abbrev-table-from-db (l)
-  (when l
-    (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
-	   (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-	   (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-	   (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion 
-	   )
-      (if e2 (cons `(,e2 ,e3 holes-abbrev-complete) 
-		   (coq-build-abbrev-table-from-db tl))
-	(coq-build-abbrev-table-from-db tl)))))
-
-
-
-
-
-
-
-
-
+  (let* ((l db) (res ())
+	(wdth (+ 2 (max-length-db coq-tactics-db)))
+	(sz (or size 30)) (lgth (length l)))
+    (while l
+      (if (<= lgth sz)
+	  (setq res 
+		(nconc res (list (cons (coq-build-title-menu l lgth)
+				       (coq-build-menu-from-db-internal l lgth wdth)))))
+	(setq res 
+	      (nconc res (list (cons (coq-build-title-menu l sz)
+				     (coq-build-menu-from-db-internal l sz wdth))))))
+      (setq l (nthcdr sz l))
+      (setq lgth (length l)))
+    res))
+
+(defun coq-build-abbrev-table-from-db (db)
+  (let ((l db) (res ()))
+    (while l
+      (let* ((hd (car l))(tl (cdr l))	; hd is a list of length 3 or 4
+	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
+	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
+	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion 
+	     )
+	(when e2 (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete)))))
+	(setq l tl)))
+    res))
+
+(message "coq-abbrev partly loaded 12")
 
 (defconst coq-tactics-menu 
   (append '("INSERT TACTICS" 
 	    ["Intros (smart)" coq-insert-intros t])
 	  (coq-build-menu-from-db coq-tactics-db)))
 
+(message "coq-abbrev partly loaded 13")
+
+
 (defconst coq-tactics-abbrev-table 
   (coq-build-abbrev-table-from-db coq-tactics-db))
 
+(message "coq-abbrev partly loaded 14")
+
 (defconst coq-tacticals-menu 
   (append '("INSERT TACTICALS" 
 	    ["Intros (smart)" coq-insert-intros t])
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 323f0f03..267e5a95 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -36,36 +36,35 @@ version of coq by doing 'coqtop -v'." )
 ;;FIXME: how to make compilable?
 (unless (noninteractive);; DA: evaluating here gives error during compile
   (let* 
-		(
-		 (seedoc (concat " (to force another version, see for example"
-							  " C-h v `coq-version-is-V8-0)'."))
-		 (v80 (concat "proofgeneral is in coq 8.0 mode" seedoc))
-		 (v81 (concat "proofgeneral is in coq 8.1 mode" seedoc))
-		 (err (concat "Both config variables coq-version-is-V8-1 and"
-						  " coq-version-is-V8-0 are set to true. This is"
-						  "contradictory.")))
-	 
-	 (cond
-	  ((and coq-version-is-V8-1 coq-version-is-V8-0) 
-		(error err))
-	  (coq-version-is-V8-1 (message v81))
-	  (coq-version-is-V8-0 (message v80))
-	  (coq-version-is-V8 (setq coq-version-is-V8-0 t coq-version-is-V8-1 nil)
-								(message v80))
-	  (t;; otherwise do coqtop -v and see which version we have
-		(let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
-		       ;; this match sets match-string below
-		       (ver (string-match "version \\([.0-9]*\\)" str)))
-		  (message str)
-		  (let ((num (and ver (match-string 1 str))))
-		    (cond
-		     ((and num (string-match "\\<8.1" num))
-		      (message v81)
-		      (setq coq-version-is-V8-1 t))
-		     (t ;; temporary, should be 8.1 when it is officially out
-		      (message (concat "Falling back to default: " v80))
-		      (setq coq-version-is-V8-0 t)))))))))
-		      
+      (
+       (seedoc (concat " (to force another version, see for example"
+                       " C-h v `coq-version-is-V8-0)'."))
+       (v80 (concat "proofgeneral is in coq 8.0 mode" seedoc))
+       (v81 (concat "proofgeneral is in coq 8.1 mode" seedoc))
+       (err (concat "Both config variables coq-version-is-V8-1 and"
+                    " coq-version-is-V8-0 are set to true. This is"
+                    "contradictory.")))
+    (cond
+     ((and coq-version-is-V8-1 coq-version-is-V8-0) 
+      (error err))
+     (coq-version-is-V8-1 (message v81))
+     (coq-version-is-V8-0 (message v80))
+     (coq-version-is-V8 (setq coq-version-is-V8-0 t coq-version-is-V8-1 nil)
+                        (message v80))
+     (t;; otherwise do coqtop -v and see which version we have
+      (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
+             ;; this match sets match-string below
+             (ver (string-match "version \\([.0-9]*\\)" str)))
+        (message str)
+        (let ((num (and ver (match-string 1 str))))
+          (cond
+           ((and num (string-match "\\<8.1" num))
+            (message v81)
+            (setq coq-version-is-V8-1 t))
+           (t;; temporary, should be 8.1 when it is officially out
+            (message (concat "Falling back to default: " v80))
+            (setq coq-version-is-V8-0 t)))))))))
+
 
 ;;; keyword databases
 
@@ -106,22 +105,23 @@ not appear in the menu but only in when calling `coq-insert-tactic'." )
 
 
 
-
-(defun coq-build-regexp-list-from-db (l &optional filter)
+(defun coq-build-regexp-list-from-db (db &optional filter)
   "Take a keyword database L and return the list of regexps for font-lock."
-  (when l
-    (let* ((hd (car l))(tl (cdr l))	; hd is the first infos list
-	   (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-	   (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-	   (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion 
-	   (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-	   (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-	   )
-      (when filter (message "funcall %S %S = %s" filter hd (funcall filter hd)))
-      ;; TODO delete doublons
-      (if (and e5 (or (not filter) (funcall filter hd)))
-	  (cons e5 (coq-build-regexp-list-from-db tl filter))
-	(coq-build-regexp-list-from-db tl filter)))))
+  (let ((l db) (res ()))
+    (while l
+      (let* ((hd (car l))(tl (cdr l))	; hd is the first infos list
+             (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
+             (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
+             (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion 
+             (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
+             (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
+             )
+        ;; TODO delete doublons
+        (when (and e5 (or (not filter) (funcall filter hd)))
+          (setq res (nconc res (list e5))))
+        (setq l tl)))
+    res
+    ))
 
 (defun filter-state-preserving (l)
   (not (nth 3 l))) ; fourth argument is nil --> state preserving command
@@ -698,11 +698,11 @@ Used by `coq-goal-command-p'"
 (defvar coq-keywords-kill-goal 
   '("Abort"))
 
-
 ;; Following regexps are all state changing
 (defvar coq-keywords-state-changing-misc-commands
   (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing))
 
+
 (defvar coq-user-keywords-state-changing-commands
   (coq-build-regexp-list-from-db coq-user-commands-db 'filter-state-changing))
 
@@ -724,6 +724,7 @@ Used by `coq-goal-command-p'"
 	coq-keywords-goal
 	coq-user-keywords-state-changing-commands))
 
+
 ;; 
 (defvar coq-keywords-state-preserving-commands
   (coq-build-regexp-list-from-db 
@@ -861,6 +862,8 @@ idtac (Nop) tactic, put the following line in your .emacs:
    (cons "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" 'font-lock-type-face))
   "*Font-lock table for Coq terms.")
 
+
+
 ;; According to Coq, "Definition" is both a declaration and a goal.
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
@@ -903,6 +906,7 @@ idtac (Nop) tactic, put the following line in your .emacs:
 	  ))
 
 
+
 (defvar coq-font-lock-keywords-1
    (append
     coq-font-lock-terms
@@ -963,6 +967,9 @@ idtac (Nop) tactic, put the following line in your .emacs:
 		  1))
 	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
 
-
 (provide 'coq-syntax)
 ;;; coq-syntax.el ends here
+
+;;; Local Variables: ***
+;;; indent-tabs-mode: nil ***
+;;; End: ***
diff --git a/coq/coq.el b/coq/coq.el
index 176a589d..f00f885b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1213,7 +1213,6 @@ mouse activation."
 ;;;;;;;;;;;;;;;;;;;;;;
 
 ;; ----- coq specific menu is defined in coq-abbrev.el
-
 (require 'coq-abbrev)
 
 (defconst module-kinds-table 
@@ -1328,6 +1327,7 @@ positions."
            "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc.")))))
           )))))
 
+
 (defun coq-insert-from-db (db)
   "Ask for a keyword, with completion on list DB tactics and insert
 corresponding string with holes at point.  If a insertion function is presnet
@@ -1343,6 +1343,7 @@ for the keyword, call it instead."
       (holes-replace-string-by-holes-backward-jump pt)
       (indent-according-to-mode))))
 
+
 (defun coq-insert-tactic ()
   "Ask for a tactic name, with completion on a quasi-exhaustive list of coq
 tactics and insert it at point.  Questions may be asked to the user."