From e09aad88fb9c92b7e10483e8c44fbf9d45b8a232 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Mon, 30 Oct 2000 14:53:43 +0000 Subject: *** empty log message *** --- af2/af2-fun.el | 19 ++++++++++++++----- af2/af2.el | 12 ++++++++++-- af2/example.af2 | 2 +- generic/proof-config.el | 28 ++++++++++++++++++++++++++-- generic/proof-script.el | 31 +++++++++++++++++++++---------- generic/proof-utils.el | 45 --------------------------------------------- 6 files changed, 72 insertions(+), 65 deletions(-) diff --git a/af2/af2-fun.el b/af2/af2-fun.el index 3a5a56f6..ff442fbc 100644 --- a/af2/af2-fun.el +++ b/af2/af2-fun.el @@ -26,14 +26,23 @@ send a compile command to af2 for the theorem which name is under the cursor." (setq af2-forget-id-command "del %s.\n" - af2-sy-definition-regexp "[ \t\n\r]\\(Cst\\|def\\)[ \t\n\r]+\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)" - af2-definition-regexp "[ \t\n\r]\\(Cst\\|def\\|claim\\|Sort\\)[ \t\n\r]+\\([^ =\\[]+\\)" + af2-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*" + af2-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)" + af2-spaces-regexp "[ \n\t\r]*" + af2-sy-definition-regexp (concat + "\\(Cst\\|def\\)" + af2-comments-regexp + "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") + af2-definition-regexp (concat + "\\(Cst\\|def\\|claim\\|Sort\\)" + af2-comments-regexp + af2-ident-regexp) ) (defun af2-find-and-forget (span) (let (str ans tmp (lsp -1)) (while span - (setq str (proof-remove-comment (span-property span 'cmd))) + (setq str (span-property span 'cmd)) (cond @@ -46,11 +55,11 @@ send a compile command to af2 for the theorem which name is under the cursor." ((proof-string-match af2-sy-definition-regexp str) (setq ans (concat (format af2-forget-id-command - (concat "$" (match-string 4 str))) ans))) + (concat "$" (match-string 7 str))) ans))) ((proof-string-match af2-definition-regexp str) (setq ans (concat (format af2-forget-id-command - (match-string 2 str)) ans)))) + (match-string 5 str)) ans)))) (setq lsp (span-start span)) diff --git a/af2/af2.el b/af2/af2.el index 1bb523c7..10dd0573 100644 --- a/af2/af2.el +++ b/af2/af2.el @@ -113,8 +113,16 @@ proof-state-command "goals." proof-goal-command-regexp "goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem" proof-save-command-regexp "save" - proof-goal-with-hole-regexp "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)[ \n\t\r]+\\([^ \n\t\r]+\\)" - proof-save-with-hole-regexp "save[ \n\t\r]+\\(\\([^ \n\t\r]+\\)\\)" + proof-goal-with-hole-regexp (concat + "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)" + af2-comments-regexp + af2-ident-regexp) + proof-goal-with-hole-result 5 + proof-save-with-hole-regexp (concat + "save" + af2-comments-regexp + af2-ident-regexp) + proof-save-with-hole-result 4 proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror" proof-non-undoables-regexp "undo" proof-goal-command "goal %s." diff --git a/af2/example.af2 b/af2/example.af2 index 4dc3abb7..36ece411 100644 --- a/af2/example.af2 +++ b/af2/example.af2 @@ -4,6 +4,6 @@ $Id$ *) -prop test /\X (X -> X). +prop (* test *) (* just un test *) test /\X (X -> X). trivial. save. \ No newline at end of file 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 -- cgit v1.2.3