From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 dev/tools/Makefile.common          |  0
 dev/tools/anomaly-traces-parser.el | 28 ++++++++++++++++++++++++++++
 2 files changed, 28 insertions(+)
 delete mode 100644 dev/tools/Makefile.common
 create mode 100644 dev/tools/anomaly-traces-parser.el

(limited to 'dev/tools')

diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common
deleted file mode 100644
index e69de29b..00000000
diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el
new file mode 100644
index 00000000..68f54266
--- /dev/null
+++ b/dev/tools/anomaly-traces-parser.el
@@ -0,0 +1,28 @@
+;; 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)
-- 
cgit v1.2.3