Added completion to insert Require, based on coq-load-path.

2 files changed, 33 insertions, 10 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index c279e91b..bc194d74 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -20,7 +20,7 @@
 
 (defconst coq-tactics-menu
   (append '("Tactics (menu)"
-	    ["Intros (smart)" coq-insert-intros t])
+	    ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."])
 	  (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db))))
 
 (defconst coq-tactics-abbrev-table
@@ -80,6 +80,10 @@
 (defpgdefault menu-entries
   `(
     ["Toggle 3 windows mode" proof-three-window-toggle t]
+    ["Toggle tooltips" proof-output-tooltips-toggle
+     :style toggle
+     :selected proof-output-tooltips
+     :help "Toggles tooltips (popup when hovering commands).\nSet `proof-output-tooltips' to nil to disable it by default."]
      ""
     ["Print..." coq-Print t]
     ["Check..." coq-Check t]
@@ -118,16 +122,16 @@
      )
      ""
     ("INSERT"
+     ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]
      ""
      ["tactic (interactive)" coq-insert-tactic t]
-     ,coq-tactics-menu
      ["tactical (interactive)" coq-insert-tactical t]
-     ,coq-tacticals-menu
-     ""
      ["command (interactive)" coq-insert-command t]
-     ,coq-commands-menu
-     ""
      ["term (interactive)" coq-insert-term t]
+     ""
+     ,coq-tactics-menu
+     ,coq-tacticals-menu
+     ,coq-commands-menu
      ,coq-terms-menu
      ""
      ["Module/Section (smart)" coq-insert-section-or-module t]
diff --git a/coq/coq.el b/coq/coq.el
index 3e94b534..d4f24ada 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2145,6 +2145,24 @@ mouse activation."
   '(("" 1) (":" 2) ("<:" 3))
   "Enumerates the different kinds of type information for modules.")
 
+(defun coq-postfix-.v-p (s)
+  (string-match-p "\\.v\\'" s))
+
+(defun coq-directories-files (l)
+  (let* ((file-list-list (mapcar 'directory-files l))
+         (file-list (apply 'append file-list-list))
+         (filtered-list (remove-if-not 'coq-postfix-.v-p file-list)))
+  filtered-list))
+
+(defun coq-remove-dot-v-extension (s)
+  (substring s 0 -2))
+
+;; TODO cleanup composed elements of coq-load-path (-R option)
+(defun coq-build-accessible-modules-list ()
+  (let* ((pth (or coq-load-path '(".")))
+         (file-list (coq-directories-files pth)))
+    (mapcar 'coq-remove-dot-v-extension file-list)))
+
 (defun coq-insert-section-or-module ()
   "Insert a module or a section after asking right questions."
   (interactive)
@@ -2178,10 +2196,11 @@ mouse activation."
           (completing-read
            "Command (TAB to see list, default Require Export) : "
            reqkinds-kinds-table nil nil nil nil "Require Export")))
-    (setq s (read-string  "Name (empty to stop) : "))
-    (while (not (string-equal s ""))
-      (insert (format "%s %s.\n" reqkind s))
-      (setq s (read-string  "Name (empty to stop) : ")))))
+    (loop do
+          (setq s (completing-read "Name (empty to stop) : "
+                                   (coq-build-accessible-modules-list)))
+          (unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s)))
+          while (not (string-equal s "")))))
 
 (defun coq-end-Section ()
   "Ends a Coq section."