Added the coq-user-... elisp customization variables to allow the user

to defclare new commands and tactics:  must typically be customized in
.emacs.

2 files changed, 134 insertions, 38 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index b67da0f5..b5993547 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -62,14 +62,42 @@
 (defvar coq-keywords-kill-goal '(
 "Abort"
 ))
-;; commands that have to be counted when undoing
-(defvar coq-keywords-undoable-commands
-  '(
-"Focus"
-))
 
-(defvar coq-keywords-not-undoable-not-backable-commands
-  '(
+
+
+
+(defcustom coq-user-backable-commands nil
+ 
+"Configuration variable (default to nil). List of strings containing
+the user defined Coq commands that need to be backtracked (like
+Require, Definition, etc).
+
+For example if MyHint and MyRequire are user defined variants of the
+Hint and Require commands, put the following line in your .emacs:
+
+(setq coq-user-backable-commands 
+		'(\"MyHint\" \"MyRequire\"))
+"
+)
+
+(defvar coq-user-non-backable-commands nil
+ 
+"Configuration variable (default to nil). List of strings containing
+the user defined Coq commands that do not need to be backtracked (like
+Print, Check, Show etc).
+
+For example if MyPrint and MyCheck are user defined variants of the
+Print and Check commands, put the following line in your .emacs:
+
+(setq coq-user-non-backable-commands 
+		'(\"MyPrint\" \"MyCheck\"))
+"
+)
+
+;; 
+
+(defvar coq-keywords-non-backable-commands
+  (append '(
 "(*" ;;Pierre comments must not be undone
 "Add\\s-+LoadPath"
 "Add\\s-+Rec\\s-+LoadPath"
@@ -82,6 +110,7 @@
 "End\\s-+Silent"
 "Eval"
 "Extraction"
+"Focus" ;; ???
 "Locate\\s-+File"
 "Locate\\s-+Library"
 "Locate"
@@ -106,17 +135,17 @@
 "Show\\s-+Proof"
 "Show\\s-+Script"
 "Show"
-	 )
+"Unfocus" ; ???
 )
+			 coq-user-non-backable-commands
+			 )
+  )
 
 
 
 
-
-
-
-(defvar coq-keywords-backable-commands
-  '(
+(defvar coq-keywords-backable-misc-commands
+ '(
 "Begin\\s-+Silent"
 "Class"
 "Coercion"
@@ -139,22 +168,41 @@
 "Require"
 "Syntax"
 "Transparent"
-	 )
-)
-
-(defvar coq-keywords-not-undoable-commands
-  (append coq-keywords-backable-commands coq-keywords-not-undoable-not-backable-commands)
 )
+ )
 
+(defvar coq-keywords-backable-commands
+  (append
+	coq-keywords-backable-misc-commands
+	coq-keywords-decl
+	coq-keywords-defn
+	coq-keywords-goal
+	coq-user-backable-commands
+	)
+  )
 
 (defvar coq-keywords-commands
-  (append coq-keywords-not-undoable-commands  coq-keywords-undoable-commands)
+  (append coq-keywords-backable-commands
+			 coq-keywords-non-backable-commands)
   "All commands keyword")
 
 
+(defcustom coq-user-undoable-tactics nil
+ 
+"Configuration variable (default to nil). List of strings containing
+the user defined Coq tactics that need to be backtracked (like almost
+all tactics, but \"Proof\").
 
-(defvar coq-tactics
-  '(
+For example if MyIntro and MyElim are user defined variants of the
+Intro and Elim tactics, put the following line in your .emacs:
+
+(setq coq-user-undoable-tactics
+		'(\"MyIntro\" \"MyElim\"))
+"
+)
+
+(defvar coq-undoable-tactics
+ (append  '(
 "Absurd"
 "Apply"
 "Assert"
@@ -224,7 +272,46 @@
 "Transitivity"
 "Trivial"
 "Unfold"
-))
+)
+coq-user-undoable-tactics
+)
+
+)
+
+(defcustom coq-user-non-undoable-tactics nil
+ 
+"Configuration variable (default to nil). List of strings containing
+the user defined Coq tactics that do not need to be backtracked (like
+\"Proof\" (no other one to my knowledge ?)).
+
+For example if MyProof and Do_nthing are user defined variants of the
+Proof (Nop) tactic, put the following line in your .emacs:
+
+(setq coq-user-non-undoable-tactics
+		'(\"MyProof\" \"Do_nthing\"))
+"
+)
+
+(defvar coq-non-undoable-tactics 
+  (append '(
+"Proof"
+)
+			 coq-user-non-undoable-tactics
+)
+)
+
+(defvar coq-tactics 
+  (append coq-undoable-tactics coq-non-undoable-tactics))
+
+
+(defvar coq-retractable-instruct
+  (append coq-undoable-tactics coq-keywords-backable-commands)
+  )
+
+(defvar coq-non-retractable-instruct
+  (append coq-non-undoable-tactics
+			 coq-keywords-non-backable-commands)
+  )
 
 (defvar coq-keywords
   (append coq-keywords-goal coq-keywords-save coq-keywords-decl
diff --git a/coq/coq.el b/coq/coq.el
index 2bf42d8c..52222ac3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -117,12 +117,22 @@
 (defconst coq-forget-id-command "Reset %s.")
 (defconst coq-back-n-command "Back %s. ") ; Pierre: added 
 
-(defconst coq-undoable-commands-regexp (proof-ids-to-regexp (append coq-tactics coq-keywords-undoable-commands)))
 
-(defconst coq-not-undoable-commands-regexp (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-not-undoable-commands)))
 
-(defconst coq-backable-commands-regexp (proof-ids-to-regexp coq-keywords-backable-commands))
-(defconst coq-not-undoable-not-backable-commands-regexp (proof-ids-to-regexp coq-keywords-not-undoable-not-backable-commands))
+(defconst coq-undoable-tactics-regexp 
+  (proof-ids-to-regexp coq-undoable-tactics))
+(defconst coq-non-undoable-tactics-regexp 
+  (proof-ids-to-regexp coq-non-undoable-tactics))
+(defconst coq-tactics-regexp
+  (proof-ids-to-regexp coq-tactics))
+(defconst coq-backable-commands-regexp
+  (proof-ids-to-regexp coq-keywords-backable-commands))
+(defconst coq-non-backable-commands-regexp 
+  (proof-ids-to-regexp coq-keywords-non-backable-commands))
+(defvar coq-retractable-instruct-regexp 
+  (proof-ids-to-regexp coq-retractable-instruct))
+(defvar coq-non-retractable-instruct-regexp
+  (proof-ids-to-regexp coq-non-retractable-instruct))
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -157,8 +167,6 @@
 ;;
 ;; FIXME Papageno 05/1999: must take sections in account.
 ;;
-;; Pierre modified the test with proof-string-match, this way new tactics
-;; can be undone (I also added "(*" in not-undoable-commands)
 (defun coq-count-undos (span)
   "Count number of undos in a span, return the command needed to undo that far."
   (let ((ct 0) str i)
@@ -170,10 +178,10 @@
       (while span
 	(setq str (span-property span 'cmd))
 	(cond ((eq (span-property span 'type) 'vanilla)
-	       (if (not (proof-string-match coq-not-undoable-commands-regexp str))
-		   (setq ct (+ 1 ct))))
+	       (if (proof-string-match coq-undoable-tactics-regexp str)
+				  (setq ct (+ 1 ct))))
 	      ((eq (span-property span 'type) 'pbp)
-	       (cond ((not (proof-string-match coq-not-undoable-commands-regexp str))
+	       (cond ((proof-string-match coq-undoable-tactics-regexp str)
 		      (setq i 0)
 		      (while (< i (length str))
 			(if (= (aref str i) proof-terminal-char)
@@ -253,15 +261,18 @@
 		 ; It is impossible to guess if a user defined command is
 		 ; backable.  This negative test bets on the fact that user
 		 ; defined commands are probably backable, which is not sure at
-		 ; all. Betting on the opposite is also wrong.
+		 ; all. Betting on the opposite is also wrong. I made the 
+		 ; user definable elisp variables coq-user... to avoid this
+		 ; problem anyway.
 		 ((and 
 			(not (coq-goal-command-p str)) ;; saved goals are catched before this point
-			(not (proof-string-match ;; now we should match all things that deal with Back
-					(concat "\\`\\(" coq-undoable-commands-regexp "\\)")
+			;; now we should match all things that do not deal with Back
+			(not (proof-string-match 
+					(concat "\\`\\(" coq-tactics-regexp "\\)")
 				  str))
 			(not (proof-string-match 
 					(concat "\\`\\(" 
-							  coq-not-undoable-not-backable-commands-regexp
+							  coq-non-backable-commands-regexp
 							  "\\)")
 					str)))
 			(setq nbacks (+ nbacks 1)))
@@ -275,8 +286,6 @@
 	 (if (null answers) proof-no-command (apply 'concat answers))
   ))
 
-;  (or ans proof-no-command)
-
   
   
 
@@ -322,7 +331,7 @@
 ; 	  (proof-lock-unlocked)))))
 
 (defun coq-state-preserving-p (cmd)
-  (not (proof-string-match coq-undoable-commands-regexp cmd)))
+  (not (proof-string-match coq-retractable-instruct-regexp cmd)))
 
 (defun coq-global-p (cmd)
   (or (proof-string-match coq-keywords-decl-defn-regexp cmd)