From 40d4ccebf9a35aa65ad163a1527405196c1710c4 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Fri, 15 Sep 2000 13:50:35 +0000 Subject: added proper call to proof-remove-comment before matching with proof-xxx-with-hole-regexp --- generic/proof-script.el | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'generic/proof-script.el') diff --git a/generic/proof-script.el b/generic/proof-script.el index 7ad8ac6b..fb8d1199 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -990,6 +990,7 @@ 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 (proof-string-match proof-save-with-hole-regexp cmd) (setq nam (match-string 2 cmd))) @@ -1010,11 +1011,11 @@ 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. - (unless nam - (and proof-goal-with-hole-regexp - (proof-string-match proof-goal-with-hole-regexp - (span-property gspan 'cmd)) - (setq nam (match-string 2 (span-property gspan 'cmd))))) + (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))))) ;; As a final desparate attempt, set the name to ;; proof-unnamed-theorem-name (Coq actually uses a default @@ -1141,10 +1142,11 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; Try to set a name from the goal ;; (useless for provers like Isabelle) - (and proof-goal-with-hole-regexp - (proof-string-match proof-goal-with-hole-regexp - (span-property gspan 'cmd)) - (setq nam (match-string 2 (span-property gspan 'cmd)))) + (let ((cmdstr (proof-remove-comment (span-property gspan 'cmd)))) + (and proof-goal-with-hole-regexp + (proof-string-match proof-goal-with-hole-regexp cmdstr) + (setq nam (match-string 2 cmdstr)))) + ;; As a final desparate attempt, set the name to "Unnamed_thm". (unless nam (setq nam proof-unnamed-theorem-name)) -- cgit v1.2.3