diff options
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-config.el | 28 | ||||
-rw-r--r-- | generic/proof-script.el | 31 | ||||
-rw-r--r-- | generic/proof-utils.el | 45 |
3 files changed, 47 insertions, 57 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 1c7b75f7..176cb84e 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -921,7 +921,9 @@ NB: This setting is not used for matching output from the prover." (defcustom proof-save-with-hole-regexp nil "Regexp which matches a command to save a named theorem. -Match number 2 should be the name of the theorem saved. +The name of the theorem is build from the variable +proof-save-with-hole-result using the same convention as +query-replace-regexp. Used for setting names of goal..save regions and for default function-menu configuration in proof-script-find-next-entity. @@ -929,6 +931,16 @@ It's safe to leave this setting as nil." :type 'regexp :group 'proof-script) +(defcustom proof-save-with-hole-result 2 + "String or Int: how to build the theorem name after matching +with proof-save-with-hole-regexp. If it is an int N use match-string +to recover the value of the Nth parenthesis matched. If it is a string +use replace-match. It the later case, proof-save-with-hole-regexp should +match the entire command" + + :type '(choice string int) + :group 'proof-script) + ;; FIXME: unify uses so that proof-anchor-regexp works sensibly (defcustom proof-goal-command-regexp nil "Matches a goal command in the proof script. @@ -941,7 +953,9 @@ for `proof-script-next-entity-regexps' used for function menus." (defcustom proof-goal-with-hole-regexp nil "Regexp which matches a command used to issue and name a goal. -Match number 2 should be the name of the goal issued. +The name of the theorem is build from the variable +proof-goal-with-hole-result using the same convention as +query-replace-regexp. Used for setting names of goal..save regions and for default function-menu configuration in proof-script-find-next-entity. @@ -949,6 +963,16 @@ It's safe to leave this setting as nil." :type 'regexp :group 'proof-script) +(defcustom proof-goal-with-hole-result 2 + "String or Int: how to build the theorem name after matching +with proof-goal-with-hole-regexp. If it is an int N use match-string +to recover the value of the Nth parenthesis matched. If it is a string +use replace-match. It the later case, proof-goal-with-hole-regexp should +match the entire command" + + :type '(choice string int) + :group 'proof-script) + (defcustom proof-non-undoables-regexp nil "Regular expression matching commands which are *not* undoable. Used in default functions `proof-generic-state-preserving-p' diff --git a/generic/proof-script.el b/generic/proof-script.el index 36423c20..fa1f4d0e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1004,11 +1004,15 @@ 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 + (message 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))) - + (setq nam + (if (stringp proof-save-with-hole-result) + (replace-match proof-save-with-hole-result nil nil cmd) + (match-string proof-save-with-hole-result cmd)))) + (message nam) ;; Search backwards for first goal command, ;; deleting spans along the way. (setq gspan span) @@ -1026,12 +1030,15 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; If the name isn't set, try to set it from the goal. (unless nam - (and proof-goal-with-hole-regexp - (let ((cmdstr - (proof-remove-comment (span-property gspan 'cmd)))) + (let ((cmdstr (span-property gspan 'cmd))) + (message cmdstr) + (and proof-goal-with-hole-regexp (proof-string-match proof-goal-with-hole-regexp cmdstr) - (setq nam (match-string 2 cmdstr))))) - + (setq nam + (if (stringp proof-goal-with-hole-result) + (replace-match proof-goal-with-hole-result nil nil cmdstr) + (match-string proof-goal-with-hole-result cmdstr)))))) + ;; As a final desparate attempt, set the name to ;; proof-unnamed-theorem-name (Coq actually uses a default ;; name for unnamed theorems, believe it or not, and issues @@ -1157,10 +1164,14 @@ 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) - (let ((cmdstr (proof-remove-comment (span-property gspan 'cmd)))) + (let ((cmdstr (span-property gspan 'cmd))) + (message cmdstr) (and proof-goal-with-hole-regexp (proof-string-match proof-goal-with-hole-regexp cmdstr) - (setq nam (match-string 2 cmdstr)))) + (setq nam + (if (stringp proof-goal-with-hole-result) + (replace-match proof-goal-with-hole-result nil nil cmdstr) + (match-string proof-goal-with-hole-result cmdstr))))) ;; As a final desparate attempt, set the name to "Unnamed_thm". (unless nam diff --git a/generic/proof-utils.el b/generic/proof-utils.el index e09dea34..942acd42 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -672,50 +672,5 @@ If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path." (setq autoload-package-name "proof") (setq generated-autoload-file "proof-autoloads.el") -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; The following function removes comments from a string. Nested -;; comments should work. Warning the length of the resulting -;; string is reduced, it may be better to replace comments by -;; white spaces - -(defun proof-remove-comment (str) - "proof-remove-comment str: return the string str with all comments removed. Nested comments should work." - (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 |