diff options
-rw-r--r-- | generic/proof-script.el | 9 | ||||
-rw-r--r-- | generic/proof-utils.el | 60 |
2 files changed, 40 insertions, 29 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index fe6c07ac..36423c20 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1004,8 +1004,8 @@ the ACS is marked in the current buffer. If CMD does not match any, (let (nam gspan next) ;; Try to set the name of the theorem from the save - (setq cmd (proof-remove-comment cmd)) (and proof-save-with-hole-regexp + (setq cmd (proof-remove-comment cmd)) (proof-string-match proof-save-with-hole-regexp cmd) (setq nam (match-string 2 cmd))) @@ -1025,11 +1025,12 @@ the ACS is marked in the current buffer. If CMD does not match any, "Proof General: script management confused, couldn't find goal span for save.") ;; If the name isn't set, try to set it from the goal. - (let ((cmdstr (proof-remove-comment (span-property gspan 'cmd)))) (unless nam (and proof-goal-with-hole-regexp - (proof-string-match proof-goal-with-hole-regexp cmdstr) - (setq nam (match-string 2 cmdstr))))) + (let ((cmdstr + (proof-remove-comment (span-property gspan 'cmd)))) + (proof-string-match proof-goal-with-hole-regexp cmdstr) + (setq nam (match-string 2 cmdstr))))) ;; As a final desparate attempt, set the name to ;; proof-unnamed-theorem-name (Coq actually uses a default diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 35f86bf9..e09dea34 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -681,31 +681,41 @@ If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path." (defun proof-remove-comment (str) "proof-remove-comment str: return the string str with all comments removed. Nested comments should work." - (if str (let - ((astr "") - (pos 0) - (lpos 0) - (spos -1) - (epos -1) - (lvl 0)) - (while (or spos epos) - (setq - spos (if (and spos (< spos lpos)) - (string-match proof-comment-start-regexp str lpos) spos) - epos (if (and epos (< epos lpos)) - (string-match proof-comment-end-regexp str lpos) epos)) - (if (and spos (or (not epos) (< spos epos))) - (progn - (if (= lvl 0) (setq astr - (concat astr - (substring str pos spos)))) - (setq lpos (+ spos 1) lvl (+ lvl 1))) - (if (epos) - (progn - (setq lpos (+ epos 1) lvl (if (> lvl 0) (- lvl 1) 0)) - (if (= lvl 0) (setq pos (+ epos 2))))))) - (setq astr (concat astr (substring str pos))) - astr))) + (if (and str proof-comment-start-regexp proof-comment-end-regexp) + (let + ((astr "") ; the result string + (regexp1 (concat "\\(\"\\)\\|\\(" + proof-comment-start-regexp "\\)\\|\\(" + proof-comment-end-regexp "\\)")) + (regexp2 (concat "\\(\"\\)")) + (pos 0) ; position of the previous match + (mpos 0) ; position of the current match + (lpos 0) ; start of the substring not in a comment and not + ; yet in astr + (lvl 0) ; number of level of comments + (in-string nil) ; are we in a string + ) + (while mpos + (setq mpos + (proof-string-match (if in-string regexp2 regexp1) str pos)) + (cond + ((match-string 1 str) + (setq pos (+ mpos 1) in-string (not in-string))) + ((match-string 2 str) + (progn + (if (= lvl 0) + (setq astr (concat astr + (substring str lpos mpos)))) + (setq pos (+ mpos 1) lvl (+ lvl 1)))) + ((match-string 3 str) + (progn + (setq pos (+ mpos 1) lvl (- lvl 1)) + (if (< lvl 0) (error "End comment not closing a start comment")) + (if (= lvl 0) + (setq lpos + (+ mpos (length (match-string 2 str))))))))) + (setq astr (concat astr (substring str pos))) + astr))) ;; End of proof-utils.el (provide 'proof-utils)
\ No newline at end of file |