From 543c2807aec1182b9a006abd233548f3459a02c6 Mon Sep 17 00:00:00 2001
From: Philipp G. Haselwarter
Date: Thu, 18 Jun 2020 15:46:20 +0100
Subject: Use `proof-shell-string-match-safe` to avoid failing on `nil` regexp

Fixes a regression introduced in 22681a3caf2c8f45700585ea74dffbf48bb2ac19.

In particular, the Coq module seems to be the only one currently setting
`proof-show-proof-diffs-regexp`, causing an error for EasyCrypt.
---
 generic/proof-shell.el | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 78b36ee7..af9b50e0 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1197,7 +1197,9 @@ contains only invisible elements for Prooftree synchronization."
 	 	    (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item)))
 	 	    proof-action-list)
 	 	   ;; If the last command in proof-action-list is a "Show Proof" form then return t
-	 	   (when last-command (string-match-p proof-show-proof-diffs-regexp last-command)))))))))
+	 	   (when last-command
+             (proof-shell-string-match-safe
+              proof-show-proof-diffs-regexp last-command)))))))))
 
 
 (defun proof-shell-insert-loopback-cmd  (cmd)
-- 
cgit v1.2.3