omit proofs: emit warning on nested proofs and continue

2 files changed, 48 insertions, 25 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 011a6625..951aade2 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -720,10 +720,13 @@ the match of `proof-script-definition-end-regexp') is considered
 to be not opaque and not omitted, thus all these proof commands
 _are_ sent to the proof assistant.
 
-If a match for `proof-script-proof-start-regexp' is found before
-the next match for `proof-script-proof-end-regexp' or
-`proof-script-definition-end-regexp', an error is signaled to the
-user.
+The feature does not work for nested proofs. If a match for
+`proof-script-proof-start-regexp' is found before the next match
+for `proof-script-proof-end-regexp' or
+`proof-script-definition-end-regexp', the search for opaque
+proofs immediately stops and all commands following the previous
+match of `proof-script-proof-start-regexp' are sent verbatim to
+the proof assistant.
 
 All the regular expressions for this feature are matched against
 the commands inside proof action items, that is as strings,
diff --git a/generic/proof-script.el b/generic/proof-script.el
index e9adc199..0c4a980d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2022,14 +2022,33 @@ start is found inside a proof."
    nil
    "proof-script omit proof feature not properly configured")
   (let (result maybe-result inside-proof
-        proof-start-span-start proof-start-span-end)
-    (dolist (item vanillas (nreverse (nconc maybe-result result)))
-      (let ((cmd (mapconcat 'identity (nth 1 item) " ")))
-        (if inside-proof
-            (progn
-              (when (string-match proof-script-proof-start-regexp cmd)
+        proof-start-span-start proof-start-span-end
+        item cmd)
+    (while vanillas
+      (setq item (car vanillas))
+      ;; cdr vanillas is at the end of the loop
+      (setq cmd (mapconcat 'identity (nth 1 item) " "))
+      (if inside-proof
+          (progn
+            (if (string-match proof-script-proof-start-regexp cmd)
                 ;; found another proof start inside a proof
-                (error "found another proof start inside a proof"))
+                ;; stop omitting and pass the remainder unmodified
+                ;; the result in `result' is aggregated in reverse
+                ;; order, need to reverse vanillas
+                (progn
+                  (setq result (nconc (nreverse vanillas) maybe-result result))
+                  (setq maybe-result nil)
+                  (setq vanillas nil)
+                  ;; for Coq nobody will notice the warning, because
+                  ;; the error about nested proofs will pop up shortly
+                  ;; afterwards
+                  (display-warning
+                   '(proof-script)
+                   ;; use the end of the span, because the start is
+                   ;; usually on the preceding  line
+                   (format (concat "found second proof start at line %d"
+                                   " - are there nested proofs?")
+                           (line-number-at-pos (span-end (car item))))))
               (if (string-match proof-script-proof-end-regexp cmd)
                   (let
                       ;; Reuse the Qed span for the whole proof,
@@ -2078,20 +2097,21 @@ start is found inside a proof."
                       (setq inside-proof nil))
                   ;; normal proof command - maybe it belongs to a
                   ;; Defined, keep it separate, until we know.
-                  (push item maybe-result))))
-          ;; outside proof
-          (if (string-match proof-script-proof-start-regexp cmd)
-              (progn
-                (setq maybe-result nil)
-                ;; Keep the Proof using command in any case.
-                (push item result)
-                (setq proof-start-span-start (span-start (car item)))
-                (setq proof-start-span-end (span-end (car item)))
-                (setq inside-proof t))
-            ;; outside, no proof start - keep it unmodified
-            (push item result)))))
-    ;; return (nreverse (nconc maybe-result result)), see dolist above
-    ))
+                  (push item maybe-result)))))
+        ;; outside proof
+        (if (string-match proof-script-proof-start-regexp cmd)
+            (progn
+              (setq maybe-result nil)
+              ;; Keep the Proof using command in any case.
+              (push item result)
+              (setq proof-start-span-start (span-start (car item)))
+              (setq proof-start-span-end (span-end (car item)))
+              (setq inside-proof t))
+          ;; outside, no proof start - keep it unmodified
+          (push item result)))
+      (setq vanillas (cdr vanillas)))
+    (nreverse (nconc maybe-result result))))
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;