Various updates. coq-end-Section now works properly.

2 files changed, 50 insertions, 47 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index f5cb9a3d..93879d9f 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -16,6 +16,7 @@
 "Hypothesis"
 "Parameter[s]?"
 "Variable[s]?"
+"Global\\s-+Variable"
 ))
 
 (defvar coq-keywords-defn
@@ -74,6 +75,7 @@
 "Hint"
 "Hints"
 "Infix"
+"Initialize"
 "Implicit\\s-+Arguments\\s-+On"
 "Implicit\\s-+Arguments\\s-+Off"
 "Load"
@@ -126,6 +128,7 @@
 "Cut"
 "DHyp"
 "DInd"
+"Decompose"
 "Dependent\\s-+Inversion_clear"
 "Dependent\\s-+Inversion"
 "Destruct"
@@ -149,6 +152,7 @@
 "Left"
 "Linear"
 "Load"
+"Omega"
 "Pattern"
 "Program_all"
 "Program"
@@ -159,6 +163,7 @@
 "Replace"
 "Rewrite"
 "Right"
+"Ring"
 "Simplify_eq"
 "Simpl"
 "Specialize"
@@ -172,7 +177,7 @@
 
 (defvar coq-keywords
   (append coq-keywords-goal coq-keywords-save coq-keywords-decl
-	  coq-keywords-defn coq-keywords-commands coq-tactics)
+	  coq-keywords-defn coq-keywords-commands)
   "All keywords in a Coq script")
 
 (defvar coq-tacticals 
@@ -196,6 +201,7 @@
     "Fix"
     "if"
     "in"
+    "let"
     "of"
     "then"
     "using"
@@ -203,7 +209,6 @@
     )
   "Reserved keyworkds of Coq")
 
-
 (defvar coq-symbols
   '(
     "|"
@@ -283,6 +288,7 @@
     coq-font-lock-terms
     (list
      (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face)
+     (cons (proof-ids-to-regexp coq-tactics) 'proof-tactics-name-face)
      (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face)
      (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face)
       
@@ -291,4 +297,24 @@
      (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
      (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
 
+(defun coq-init-syntax-table ()
+  "Set appropriate values for syntax table in current buffer."
+
+  (modify-syntax-entry ?\$ ".")
+  (modify-syntax-entry ?\/ ".")
+  (modify-syntax-entry ?\\ ".")
+  (modify-syntax-entry ?+  ".")
+  (modify-syntax-entry ?-  ".")
+  (modify-syntax-entry ?=  ".")
+  (modify-syntax-entry ?%  ".")
+  (modify-syntax-entry ?<  ".")
+  (modify-syntax-entry ?>  ".")
+  (modify-syntax-entry ?\& ".")
+  (modify-syntax-entry ?_  "_")
+  (modify-syntax-entry ?\' "_")
+  (modify-syntax-entry ?\| ".")
+  (modify-syntax-entry ?\* ". 23")
+  (modify-syntax-entry ?\( "()1")
+  (modify-syntax-entry ?\) ")(4"))
+
 (provide 'coq-syntax)
diff --git a/coq/coq.el b/coq/coq.el
index 622bc2f5..22d75774 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -41,10 +41,6 @@
   :type 'string
   :group 'coq)
 
-(defconst coq-process-config "Reset Initial."
-  "Command to reset to initial state and 
-   configure pretty printing of the Coq process for emacs.")
-
 (defconst coq-interrupt-regexp "Interrupted"
   "Regexp corresponding to an interrupt")
 
@@ -67,6 +63,15 @@
   :type 'string
   :group 'coq)
 
+;; Command to initialize the Coq Proof Assistant
+(defconst coq-shell-init-cmd 
+  (concat (format "Set Undo %s." coq-default-undo-limit)
+	  (format "Cd \"%s\"." default-directory)))
+
+;; Command to reset the Coq Proof Assistant
+(defconst coq-shell-restart-cmd 
+  "Reset Initial.")
+
 (defvar coq-shell-prompt-pattern (concat "^" proof-id " < ")
   "*The prompt pattern for the inferior shell running coq.")
 
@@ -105,10 +110,11 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (define-derived-mode coq-shell-mode proof-shell-mode
-   "coq-shell" 
-   ;; With nil argument for docstring, Emacs makes up a nice one.
-   nil
-   (coq-shell-mode-config))
+   "coq-shell" nil
+
+   (coq-shell-mode-config)
+   (setq font-lock-keywords coq-font-lock-keywords-1)
+   (font-lock-mode))
 
 (define-derived-mode coq-response-mode proof-response-mode
   "CoqResp" nil
@@ -128,12 +134,6 @@
 ;;   Code that's coq specific                                      ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; FIXME da: can't this be done by proof-shell-init-cmd ?
-(defun coq-shell-init-hook ()
-  (insert (format "Set Undo %s." coq-default-undo-limit))
-  (insert (format "Cd \"%s\"." default-directory))
-  (remove-hook 'proof-shell-insert-hook 'coq-shell-init-hook))
-
 (defun coq-set-undo-limit (undos)
   (proof-shell-invisible-command (format "Set Undo %s." undos)))
 
@@ -300,11 +300,10 @@
 (defun coq-end-Section ()
   "Ends a Coq section."
   (interactive)
-  (let (count) 
+  (let ((count 1)) ; The number of section already "Ended" + 1
     (let ((section 
 	   (save-excursion 
 	     (progn 
-	       (setq count 1) ; The number of section already "Ended" + 1
 	       (while (and (> count 0) 
 			   (search-backward-regexp 
 			    "Chapter\\|Section\\|End" 0 t))
@@ -312,9 +311,9 @@
 		     (setq count (1+ count))
 		   (setq count (1- count))))
 	       (buffer-string
-		(progn (beginning-of-line) (point)) 
+		(progn (beginning-of-line) (forward-word 1) (point)) 
 		(progn (end-of-line) (point)))))))
-      (insert (replace-string "Section" "End" section)))))
+      (insert (concat "End" section)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Indentation                                                    ;;
@@ -398,27 +397,6 @@
 ;;   Configuring proof and pbp mode and setting up various utilities  ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-; FIXME: IMHO (tms) this ought to be defined in coq-syntax and not here.
-(defun coq-init-syntax-table ()
-  "Set appropriate values for syntax table in current buffer."
-
-  (modify-syntax-entry ?\$ ".")
-  (modify-syntax-entry ?\/ ".")
-  (modify-syntax-entry ?\\ ".")
-  (modify-syntax-entry ?+  ".")
-  (modify-syntax-entry ?-  ".")
-  (modify-syntax-entry ?=  ".")
-  (modify-syntax-entry ?%  ".")
-  (modify-syntax-entry ?<  ".")
-  (modify-syntax-entry ?>  ".")
-  (modify-syntax-entry ?\& ".")
-  (modify-syntax-entry ?_  "_")
-  (modify-syntax-entry ?\' "_")
-  (modify-syntax-entry ?\| ".")
-  (modify-syntax-entry ?\* ". 23")
-  (modify-syntax-entry ?\( "()1")
-  (modify-syntax-entry ?\) ")(4"))
-
 (defun coq-mode-config ()
 
   (setq proof-terminal-char ?\.)
@@ -458,10 +436,12 @@
 
   (proof-config-done)
 
+;; Coq-specific key mappings
+
   (define-key (current-local-map) [(control c) ?I] 'coq-Intros)
   (define-key (current-local-map) [(control c) ?a] 'coq-Apply)
   (define-key (current-local-map) [(control c) (control s)] 'coq-Search)
-  (define-key (current-local-map) [(control c) ?s] 'coq-Section)
+  (define-key (current-local-map) [(control c) ?s] 'coq-begin-Section)
   (define-key (current-local-map) [(control c) ?e] 'coq-end-Section)
 
 ;; outline
@@ -509,15 +489,12 @@
         proof-shell-result-end "\372 End Pbp result \373"
         proof-shell-start-goals-regexp "[0-9]+ subgoals?"
         proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
-        proof-shell-init-cmd coq-process-config
-	proof-shell-restart-cmd coq-process-config
+        proof-shell-init-cmd coq-shell-init-cmd
+	proof-shell-restart-cmd coq-shell-restart-cmd
 	proof-analyse-using-stack t
 ;;	proof-lift-global 'coq-lift-global
 	)
 
-  ;; The following hook is removed once it's called.
-  (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t)
-
   (coq-init-syntax-table)
 
   (proof-shell-config-done))