Some changes for undoing with coq, handle user-defined tactics, in

coq/coq-syntax.el and coq/coq.el.

3 files changed, 34 insertions, 17 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e4d8b984..25880fed 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -16,8 +16,10 @@
 "Hypothesis"
 "Parameter[s]?"
 ;; da: 3.2 I added Section here, to try to fix undo for Sections working
-;; better.  
-"Section"				
+;; better.
+;;Pierre : Chapter also
+"Chapter"
+"Section"
 "Variable[s]?"
 "Global\\s-+Variable"
 ;;added tactic def here because it needs Reset to be undone correctly
@@ -69,12 +71,12 @@
 
 (defvar coq-keywords-not-undoable-commands
   '(
+"(*" ;;Pierre comments must not be undone
 "Add\\s-+ML\\s-+Path"
 "AddPath"
 "Begin\\s-+Silent"
 "Cd"
 "Check"
-"Chapter"
 "Class"
 "Coercion"
 "DelPath"
diff --git a/coq/coq.el b/coq/coq.el
index d00ee90e..daa4ba8f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -43,13 +43,14 @@
 ;; Pierre: I add Print Check and PrintHint
 ;; maybe Print and Check should be buttons ?
 (defpgdefault menu-entries
-  '(["Print" coq-Print t]
-    ["Check" coq-Check t]
+  '(["Print..." coq-Print t]
+    ["Check..." coq-Check t]
     ["Hints" coq-PrintHint t]
-    ["Intros" coq-Intros t]
+    ["Intros..." coq-Intros t]
+    ["Show ith goal..." coq-Show t]
     ["Apply"  coq-Apply t]
-    ["Search isos" coq-SearchIsos t]
-    ["Begin Section" coq-begin-Section t]
+    ["Search isos..." coq-SearchIsos t]
+    ["Begin Section..." coq-begin-Section t]
     ["End Section" coq-end-Section t]
     ["Compile" coq-Compile t]))
 
@@ -90,7 +91,7 @@
 (defvar coq-outline-regexp
   (concat "(\\*\\|" (proof-ids-to-regexp 
 	   '(
-"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint"))))
+"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint" "Save" "Qed" "Defined"))))
 
 (defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.\n")
 
@@ -102,6 +103,8 @@
 
 (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 coq-keywords-not-undoable-commands))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -136,7 +139,8 @@
 ;;
 ;; FIXME Papageno 05/1999: must take sections in account.
 ;;
-
+;; Pierre modified the test with proof-string-match, this way new tactics
+;; ca 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)
@@ -148,10 +152,10 @@
       (while span
 	(setq str (span-property span 'cmd))
 	(cond ((eq (span-property span 'type) 'vanilla)
-	       (if (proof-string-match coq-undoable-commands-regexp str)
+	       (if (not (proof-string-match coq-not-undoable-commands-regexp str))
 		   (setq ct (+ 1 ct))))
 	      ((eq (span-property span 'type) 'pbp)
-	       (cond ((proof-string-match coq-undoable-commands-regexp str)
+	       (cond ((not (proof-string-match coq-not-undoable-commands-regexp str))
 		      (setq i 0)
 		      (while (< i (length str))
 			(if (= (aref str i) proof-terminal-char)
@@ -304,6 +308,15 @@ This is specific to coq-mode."
     (proof-shell-invisible-command
      (format "Check %s." cmd))))
 
+(defun coq-Show ()
+  "Ask for a number i and show the ith goal"
+  (interactive)
+  (let (cmd)
+    (proof-shell-ready-prover) 
+    (setq cmd (read-string "Show Goal number: " nil 'proof-minibuffer-history))
+    (proof-shell-invisible-command
+     (format "Show %s." cmd))))
+
 (defun coq-PrintHint ()
   "Print all hints applicable to the current goal"
   (interactive)
diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el
index 3f77c1b3..7c09b2ef 100644
--- a/coq/x-symbol-coq.el
+++ b/coq/x-symbol-coq.el
@@ -6,7 +6,9 @@
 ;;
 
 (defvar x-symbol-coq-symbol-table 
-  '((perpendicular  () "False"  "\\<bottom>")
+  '((arrowup () "\\+"  "\\<uparrow>")
+    (arrowdown () "\\-"  "\\<downarrow>")
+    (perpendicular  () "False"  "\\<bottom>")
     (top            () "True"   "\\<top>")
     (notsign       () "~"       "\\<not>")
     (longarrowright () "->"  "\\<longrightarrow>")
@@ -63,11 +65,11 @@
 (defvar x-symbol-coq-case-insensitive nil)
 
 ;Pierre: let's try this, phi1 will be encoded, but not phia or
-;philosophy. problem: blaphi will be encoded, other problem: false1
-;sholud not be encoded (this on eshould be easy:
-;x-symbol-coq-token-shape is a list)
+;philosophy. problem: blaphi will be encoded,
+; other problem: false1 sholud not be encoded
+
+(defvar x-symbol-coq-token-shape '(?_ "[A-Za-z]+" . "[A-Za-z_]"))
 
-(defvar x-symbol-coq-token-shape '(?_ "[A-Za-z]+" . "[^0-9\ \t\n]"))
 ;(defvar x-symbol-coq-token-shape nil)
 
 (defvar x-symbol-coq-table x-symbol-coq-symbol-table)