change for version 0.83 of PhoX

3 files changed, 29 insertions, 15 deletions

diff --git a/phox/phox-font.el b/phox/phox-font.el
index f34b051a..f58f41f3 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -16,7 +16,7 @@
        "I\\(mport\\|nductive\\)\\|"
        "Use\\|"
        "Sort\\|"
-       "new_\\(intro\\|elim\\|rewrite\\)\\|"
+       "new_\\(intro\\|e\\(lim\\|quation\\)\\|rewrite\\)\\|"
        "a\\(dd_path\\|uthor\\)\\|"
        "c\\(l\\(aim\\|ose_def\\)\\|or\\(ollary\\)?\\)\\|"
        "d\\(e\\(f\\(_thlist\\)?\\|l\\(_proof\\)\\)\\|ocuments\\|epend\\)\\|"
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 7592a87e..d556a3c8 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -6,7 +6,7 @@
  phox-forget-proof-command "del_proof %s.\n"
  phox-forget-new-elim-command "edel elim %s.\n"
  phox-forget-new-intro-command "edel intro %s.\n"
- phox-forget-new-rewrite-command "edel rewrite %s.\n"
+ phox-forget-new-equation-command "edel equation %s.\n"
  phox-forget-close-def-command "edel closed %s.\n"
 ; phox-comments-regexp : a sequence of comments and white spaces
  phox-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*"
@@ -54,6 +54,9 @@
  phox-new-rewrite-regexp (concat
    "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
    phox-ident-regexp)
+ phox-new-equation-regexp (concat
+   "new_equation\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]"
+   phox-ident-regexp)
  phox-close-def-regexp (concat
    "close_def"
    phox-comments-regexp
@@ -95,6 +98,7 @@ or for optional argument TABLE."
 "edel"
 "new_elim"
 "new_intro"
+"new_equation"
 "new_rewrite"
 "Data"
 "Inductive"
@@ -190,9 +194,14 @@ or for optional argument TABLE."
 	      (concat (format phox-forget-new-intro-command 
 				  (match-string 3 str)) ans)))
 
-       ((proof-string-match phox-new-rewrite-regexp str)
+       ((proof-string-match phox-new-rewrite-regexp str) ; deprecated
+	(setq ans 
+	      (concat (format phox-forget-new-equation-command 
+				  (match-string 3 str)) ans)))
+
+       ((proof-string-match phox-new-equation-regexp str)
 	(setq ans 
-	      (concat (format phox-forget-new-rewrite-command 
+	      (concat (format phox-forget-new-equation-command 
 				  (match-string 3 str)) ans)))
 
        ((proof-string-match phox-close-def-regexp str)
@@ -268,12 +277,12 @@ Gives the list of all axioms which have been used to prove the theorem."
   "Interactive function : 
 ask for a string and send an eshow command to PhoX for it. 
 
-Shows the given extension-list.  Possible extension lists are : rewrite
-(the list of rewriting rules introduced by the new_rewrite command),
-elim, intro, (the introduction and elimination rules introduced by the
-new_elim and new_intro {-t} commands), closed (closed definitions
-introduced by the close_def command) and tex (introduced by the
-tex_syntax command)."
+Shows the given extension-list.  Possible extension lists are : equation
+(the list of equations added to unification introduced by the new_equation
+command), elim, intro, (the introduction and elimination rules
+introduced by the new_elim and new_intro {-t} commands), closed
+(closed definitions introduced by the close_def command) and tex
+(introduced by the tex_syntax command)."
 
 (interactive "sextension list: ")
 (proof-shell-invisible-command (concat "eshow " extlist)))
diff --git a/phox/phox.el b/phox/phox.el
index 8b22dafe..5fadf597 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -108,14 +108,14 @@
    proof-script-comment-end               "*)"
    proof-state-command             "goals."
    proof-goal-command-regexp       
-    "\\`\\(goal[ \t\n\r]\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
+    "\\`\\(Local[ \t\n\r]+\\)?\\(goal[ \t\n\r]\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
    proof-save-command-regexp       "\\`save"
    proof-goal-with-hole-regexp  
    (concat 
-    "\\`\\(pro\\(p\\(osition\\)?\\|ve_claim\\)\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
+    "\\`\\(Local[ \t\n\r]+\\)?\\(pro\\(p\\(osition\\)?\\|ve_claim\\)\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)"
     phox-strict-comments-regexp
     phox-ident-regexp)
-   proof-goal-with-hole-result     15
+   proof-goal-with-hole-result     16
    proof-save-with-hole-regexp     
    (concat 
     "\\`save"
@@ -206,7 +206,10 @@
    font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
    proof-output-fontify-enable     t)
   (phox-sym-lock-start)
-  (add-hook 'proof-shell-handle-delayed-output-hook 'phox-sym-lock-font-lock-hook)
+  (if (and (featurep 'phox-sym-lock) phox-sym-lock)
+      (add-hook 'proof-shell-handle-delayed-output-hook 
+		'phox-sym-lock-font-lock-hook)
+    )
   (proof-response-config-done))
 
 (define-derived-mode phox-goals-mode proof-goals-mode
@@ -215,7 +218,9 @@
    font-lock-keywords  (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
    proof-output-fontify-enable     t)
   (phox-sym-lock-start)
-  (add-hook 'pg-before-fontify-output-hook 'phox-sym-lock-font-lock-hook)
+  (if (and (featurep 'phox-sym-lock) phox-sym-lock)
+      (add-hook 'pg-before-fontify-output-hook 
+		'phox-sym-lock-font-lock-hook))
   (proof-goals-config-done))
 
 ;; The response buffer and goals buffer modes defined above are