Merge anomaly-traces-parser.el into coqdev.el.

2 files changed, 16 insertions, 28 deletions

diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el
deleted file mode 100644
index 68f54266f..000000000
--- a/dev/tools/anomaly-traces-parser.el
+++ /dev/null
@@ -1,28 +0,0 @@
-;; This Elisp snippet adds a regexp parser for the format of Anomaly
-;; backtraces (coqc -bt ...), to the error parser of the Compilation
-;; mode (C-c C-c: "Compile command: ..."). Once the
-;; coq-change-error-alist-for-backtraces function has run, file
-;; locations in traces are recognized and can be jumped from easily
-;; from the *compilation* buffer.
-
-;; You can just copy everything below to your .emacs and this will be
-;; enabled from any compilation command launched from an OCaml file.
-
-(defun coq-change-error-alist-for-backtraces ()
-  "Hook to change the compilation-error-regexp-alist variable, to
-   search the coq backtraces for error locations"
-  (interactive)
-  (add-to-list
-   'compilation-error-regexp-alist-alist
-   '(coq-backtrace
-     "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
-      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
-      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
-     2 (3 . 4) (5 . 6)))
-  (add-to-list 'compilation-error-regexp-alist 'coq-backtrace))
-
-;; this Anomaly parser should be available when one is hacking
-;; on the *OCaml* code of Coq (adding bugs), so we enable it
-;; through the OCaml mode hooks.
-(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces)
-(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces)
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index f5a0feffa..31cde7584 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -82,5 +82,21 @@ Note that this function is executed before _Coqproject is read if it exists."
     (setq-local coq-prog-name (concat dir "bin/coqtop"))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
 
+;; This Elisp snippet adds a regexp parser for the format of Anomaly
+;; backtraces (coqc -bt ...), to the error parser of the Compilation
+;; mode (C-c C-c: "Compile command: ..."). File locations in traces
+;; are recognized and can be jumped from easily in the *compilation*
+;; buffer.
+(defvar compilation-error-regexp-alist-alist)
+(defvar compilation-error-regexp-alist)
+(add-to-list
+ 'compilation-error-regexp-alist-alist
+ '(coq-backtrace
+   "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\
+      lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\
+      \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)"
+   2 (3 . 4) (5 . 6)))
+(add-to-list 'compilation-error-regexp-alist 'coq-backtrace)
+
 (provide 'coqdev)
 ;;; coqdev ends here