Merged changes sent by Patrick Loiseleur.

2 files changed, 42 insertions, 21 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 16f2a15f..f9c1c8db 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,8 +1,7 @@
 ;; coq-syntax.el Font lock expressions for Coq
 ;; Copyright (C) 1997, 1998 LFCS Edinburgh. 
-;; Author: Thomas Kleymann and Healfdene Goguen
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
-;; Please let us know if you could maintain this package!
+;; Authors: Thomas Kleymann and Healfdene Goguen
+;; Maintainer: Patrick Loiseleur <Patrick.Loiseleur@lri.fr> 
 
 ;; $Id$
 
@@ -12,10 +11,11 @@
 
 (defvar coq-keywords-decl
   '(
-"Axiom"
+"Axiom[s]?"
+"Hypotheses"
 "Hypothesis"
-"Parameter"
-"Variable"
+"Parameter[s]?"
+"Variable[s]?"
 ))
 
 (defvar coq-keywords-defn
@@ -53,24 +53,39 @@
 (defvar coq-keywords-commands
   '(
 "AddPath"
+"Begin\\s-+Silent"
 "Cd"
 "Check"
 "Class"
 "Coercion"
 "DelPath"
+"End"
+"End\\s-+Silent"
 "Eval"
 "Extraction"
 "Focus"
-"Immediate"
+"Grammar"
 "Hint"
+"Hints"
 "Infix"
+"Implicit\\s-+Arguments\\s-+On"
+"Implicit\\s-+Arguments\\s-+Off"
+"Load"
+"Local\\s-+Coercion"
 "Opaque"
 "Print"
 "Proof"
 "Pwd"
+"Require\\s-+Export"
+"Require\\s-+Import"
+"Require"
 "Reset"
 "Search"
+"SearchIsos"
+"Section"
 "Show"
+"Syntax"
+"Tactic\\s-+Definition"
 "Transparent"
 ))
 
@@ -80,6 +95,7 @@
 "Apply"
 "Assumption"
 "Auto"
+"AutoRewrite"
 "Case"
 "Change"
 "Clear"
@@ -90,24 +106,22 @@
 "Cut"
 "DHyp"
 "DInd"
-"Dependent"
+"Dependent\\s-+Inversion_clear"
+"Dependent\\s-+Inversion"
 "Destruct"
 "Discriminate"
 "Double"
 "EApply"
 "EAuto"
 "Elim"
-"End"
 "Exact"
 "Exists"
 "Fix"
 "Generalize"
-"Grammar"
 "Hnf"
 "Induction"
 "Injection"
-"Intro"
-"Intros"
+"Intro[s]?"
 "Intuition"
 "Inversion_clear"
 "Inversion"
@@ -125,13 +139,11 @@
 "Replace"
 "Rewrite"
 "Right"
-"Section"
 "Simplify_eq"
 "Simpl"
 "Specialize"
 "Split"
 "Symmetry"
-"Syntax"
 "Tauto"
 "Transitivity"
 "Trivial"
@@ -144,6 +156,7 @@
   "All keywords in a Coq script")
 
 (defvar coq-tacticals '(
+"Abstract"
 "Do"
 "Idtac"
 "OrElse"
@@ -152,7 +165,7 @@
 ))
 
 ;; ----- regular expressions
-(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\)"
+(defvar coq-error-regexp "^\\(Error\\|Discarding\\|Syntax error\\|System Error\\|Anomaly\\)"
   "A regular expression indicating that the Coq process has identified
   an error.")
 
diff --git a/coq/coq.el b/coq/coq.el
index cfca4ec0..b53e4cb3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -3,7 +3,7 @@
 ;; Author: Healfdene Goguen
 ;; Maintainer: Patrick Loiseleur <Patrick.Loiseleur@lri.fr> 
 
-;; $Id$
+;; $Id$ 
 
 (require 'proof-script)
 (require 'coq-syntax)
@@ -145,10 +145,12 @@
   (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
   "Declaration and definition regexp.")
 
-;; da: this one function breaks the nice configuration of Proof General:
-;; would be nice to have proof-goal-regexp instead.
-;; Unfortunately Coq allows Goals beginning with "Definition" and the 
-;; like, so it is difficult to have just a proof-goal-regexp setting.  
+;; FIXME da: this one function breaks the nice configuration of Proof General:
+;; would like to have proof-goal-regexp instead.
+;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, 
+;; so it appears more difficult than just a proof-goal-regexp setting.
+;; Future improvement may simply to be allow a function value for
+;; proof-goal-regexp.
 
 (defun coq-goal-command-p (str)
   "Decide whether argument is a goal or not"
@@ -312,6 +314,10 @@
   (setq proof-mode-for-pbp 'coq-pbp-mode)
 )
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;   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."
@@ -399,6 +405,7 @@
   (setq proof-shell-prompt-pattern coq-shell-prompt-pattern
         proof-shell-cd coq-shell-cd
         proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp
+	proof-shell-restart-cmd "Reset Initial."
         proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp
         proof-shell-error-regexp coq-error-regexp
 	proof-shell-interrupt-regexp coq-interrupt-regexp
@@ -421,7 +428,8 @@
         proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
         proof-shell-init-cmd nil
 	proof-analyse-using-stack t
-	proof-lift-global 'coq-lift-global)
+	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)