Remove dir-locals and ship suggested helper hooks instead.

.dir-locals led to issues with unsafe local variable warnings. With
this method the user is opting in to running this code so there are no warnings.

5 files changed, 73 insertions, 45 deletions

diff --git a/.dir-locals.el b/.dir-locals.el
deleted file mode 100644
index e32ce14a4..000000000
--- a/.dir-locals.el
+++ /dev/null
@@ -1,37 +0,0 @@
-;; EMACS CONFIGURATION FOR COQ DEVELOPPERS This configuration will be
-;; executed for each opened file under coq root directory.
-((nil
-  . ((eval
-      . (progn
-	  ;; coq root directory (ending with slash)
-	  (let ((coq-root-directory (when buffer-file-name
-				      (locate-dominating-file
-				       buffer-file-name
-				       ".dir-locals.el")))
-		(coq-project-find-file
-		 (and (boundp 'coq-project-find-file) coq-project-find-file)))
-	    ;; coq tags file and coq debugger executable
-	    (set (make-local-variable 'tags-file-name)
-		 (concat coq-root-directory "TAGS"))
-	    (setq camldebug-command-name (concat coq-root-directory
-						 "dev/ocamldebug-coq"))
-
-	    ;; Setting the compilation directory to coq root. This is
-	    ;; mutually exclusive with the setting of default-directory
-	    ;; below. Also setting the path for next error.
-	    (unless coq-project-find-file
-	      (set (make-local-variable 'compile-command)
-		   (concat "make -C " coq-root-directory))
-	      (set (make-local-variable 'compilation-search-path)
-		   (cons coq-root-directory nil)))
-
-	    ;; Set default directory to coq root ONLY IF variable
-	    ;; coq-project-find-file is non nil. This should remain a
-	    ;; user preference and not be set by default. This setting
-	    ;; is redundant with compile-command above as M-x compile
-	    ;; always CD's to default directory. To enable it add this
-	    ;; to your emacs config: (setq coq-project-find-file t)
-	    (when coq-project-find-file
-	      (setq default-directory coq-root-directory))))
-      ))
-  ))
diff --git a/dev/README b/dev/README
index b446c3e97..f97e2a769 100644
--- a/dev/README
+++ b/dev/README
@@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
 Other development tools (directory tools)
 -----------------------
 
+coqdev.el: helper customizations for everyday Coq development, eg
+  making `compile' work in subdirectories
+
 objects.el: various development utilities at emacs level
+
 anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
   location of Anomaly backtraces and jump to them conveniently from
   the Emacs *compilation* output.
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
new file mode 100644
index 000000000..581995d46
--- /dev/null
+++ b/dev/tools/coqdev.el
@@ -0,0 +1,69 @@
+;;; coqdev.el --- Emacs helpers for Coq development  -*- lexical-binding:t -*-
+
+;; Copyright (C) 2018 The Coq Development Team
+
+;; Maintainer: coqdev@inria.fr
+
+;;; Commentary:
+
+;; Helpers to set compilation commands, proof general variables, etc
+;; for Coq development
+
+;; You can disable individual features without editing this file by
+;; using `remove-hook', for instance
+;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
+
+;;; Code:
+
+(require 'subr-x)
+
+(defun coqdev-default-directory ()
+  "Return the Coq repository containing `default-directory'."
+  (when-let ((dir (locate-dominating-file default-directory "META.coq")))
+    (expand-file-name dir)))
+
+(defun coqdev-setup-compile-command ()
+  "Setup `compilate-command' for Coq development."
+  (when-let ((dir (coqdev-default-directory)))
+      (setq-local compile-command (concat "make -C " dir))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command)
+
+(defvar camldebug-command-name) ; from camldebug.el (caml package)
+(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package)
+(defun coqdev-setup-camldebug ()
+  "Setup ocamldebug for Coq development.
+
+Specifically `camldebug-command-name' and `ocamldebug-command-name'."
+  (when-let ((dir (coqdev-default-directory)))
+    (setq-local camldebug-command-name (concat dir "dev/ocamldebug-coq"))
+    (setq-local ocamldebug-command-name (concat dir "dev/ocamldebug-coq"))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug)
+
+(defun coqdev-setup-tags ()
+  "Setup `tags-file-name' for Coq development."
+  (when-let ((dir (coqdev-default-directory)))
+      (setq-local tags-file-name (concat dir "TAGS"))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-tags)
+
+(defvar coq-prog-args)
+(defvar coq-prog-name)
+
+;; Lets us detect whether there are file local variables
+;; even though PG sets it with `setq' when there's a _Coqproject.
+;; Also makes sense generally, so might make it into PG someday.
+(make-variable-buffer-local 'coq-prog-args)
+(setq-default coq-prog-args nil)
+
+(defun coqdev-setup-proofgeneral ()
+  "Setup Proofgeneral variables for Coq development.
+
+Note that this function is executed before _Coqproject is read if it exists."
+  (when-let ((dir (coqdev-default-directory)))
+    (unless coq-prog-args ; In case there are file-local variables
+      (setq coq-prog-args `("-coqlib" ,dir
+                            "-R" ,(concat dir "plugins") "Coq"
+                            "-R" ,(concat dir "theories") "Coq")))
+    (setq-local coq-prog-name (concat dir "bin/coqtop"))))
+(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
+
+(provide 'coqdev)
diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el
deleted file mode 100644
index 4e8830f6c..000000000
--- a/plugins/.dir-locals.el
+++ /dev/null
@@ -1,4 +0,0 @@
-((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
-						buffer-file-name ".dir-locals.el")))
-			(setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq"))
-			(setq-local coq-prog-name (expand-file-name "../bin/coqtop")))))))
diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el
deleted file mode 100644
index 4e8830f6c..000000000
--- a/theories/.dir-locals.el
+++ /dev/null
@@ -1,4 +0,0 @@
-((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
-						buffer-file-name ".dir-locals.el")))
-			(setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq"))
-			(setq-local coq-prog-name (expand-file-name "../bin/coqtop")))))))