updating for new PG version

3 files changed, 19 insertions, 13 deletions

diff --git a/phox/phox-font.el b/phox/phox-font.el
index f58f41f3..3c313990 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -19,7 +19,7 @@
        "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\\)\\|"
+       "d\\(e\\(f\\(\\(_thlist\\|rec\\)\\)?\\|l\\(_proof\\)\\)\\|ocuments\\|epend\\)\\|"
        "e\\(lim_after_intro\\|xport\\|del\\|show\\)\\|"
        "f\\(act\\|lag\\)\\|"
        "goal\\|"
@@ -28,25 +28,29 @@
        "p\\(ath\\|r\\(int\\(_sort\\)?\\|iority\\|op\\(osition\\)?\\|ove_claim\\)\\)\\|"
        "quit\\|"
        "s\\(ave\\|earch\\)\\|"
-       "t\\(ex\\(_syntax\\)?\\|heo\\(rem\\)?\\|itle\\)"
+       "t\\(ex\\(_syntax\\)?\\|heo\\(rem\\)?\\|itle\\|ype\\)"
        "\\)[ \t\n\r.]")
       '(0 'font-lock-keyword-face t))
 ;proof command
     (cons (concat "\\([ \t]\\|^\\)\\("
-       "a\\(bort\\|fter\\|pply\\|xiom\\)\\|"
-       "by_absurd\\|"
+       "a\\(bort\\|fter\\|nd\\|pply\\|ssume\\|xiom\\)\\|"
+       "by\\(_absurd\\)?\\|"
        "constraints\\|"
        "elim\\|"
+       "deduce\\|"
+       "evaluate\\(_hyp\\)?\\|"
        "from\\|"
        "goals\\|"
        "in\\(tros?\\|stance\\)\\|"
-       "l\\(oc\\(al\\|k\\)\\|efts?\\)\\|"
+       "l\\(oc\\(al\\|k\\)\\|e\\(t\\|fts?\\)\\)\\|"
        "next\\|"
+       "of\\|"
        "prove\\|"
        "r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|"
-       "s\\(elect\\|lh\\)\\|"
-       "trivial\\|" 
-       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)" 
+       "s\\(elect\\|how\\|lh\\)\\|"
+       "t\\(hen\\|rivial\\)\\|" 
+       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)\\|" 
+       "with"
        "\\)[ \t.]")
       '(0 'font-lock-type-face t))))
 
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 12dddf42..50c0b67e 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -16,7 +16,7 @@
  phox-inductive-option "\\(\\[[^]]*]\\)?"
  phox-spaces-regexp "[ \n\t\r]*"
  phox-sy-definition-regexp (concat 
-   "\\(Cst\\|def\\)"
+   "\\(Cst\\|\\(def\\(rec\\)?\\)\\)"
    phox-comments-regexp
    "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
  phox-sy-inductive-regexp (concat 
@@ -32,13 +32,13 @@
    phox-comments-regexp
    phox-ident-regexp) 
  phox-data-regexp (concat 
-   "Data"
+   "\\(Data\\|type\\)"
    phox-comments-regexp
    phox-inductive-option
    phox-comments-regexp
    phox-ident-regexp) 
  phox-definition-regexp (concat
-   "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)"
+   "\\(Cst\\|def\\(_thlist\\|rec\\)?\\|claim\\|Sort\\)"
    phox-comments-regexp
    phox-ident-regexp)
  phox-prove-claim-regexp (concat
@@ -101,6 +101,7 @@ or for optional argument TABLE."
 "new_equation"
 "new_rewrite"
 "Data"
+"type"
 "Inductive"
 "add_path"
 "Import"
@@ -251,7 +252,7 @@ or for optional argument TABLE."
   "Process until the end of the next unprocessed command after point.
 If inside a comment, just process until the start of the comment."
   (interactive)
-  (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
+;  (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n"))
   (proof-with-script-buffer
    (proof-maybe-save-point
     (goto-char (proof-queue-or-locked-end))
diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el
index 122ccf93..ac1cb658 100644
--- a/phox/x-symbol-phox.el
+++ b/phox/x-symbol-phox.el
@@ -123,7 +123,8 @@ See `x-symbol-language-access-alist' for details."
   :type 'x-symbol-class-faces)
 
 
-(defvar x-symbol-phox-font-lock-keywords x-symbol-nomule-font-lock-keywords)
+(defvar x-symbol-phox-font-lock-keywords nil)
+
 (defvar x-symbol-phox-font-lock-allowed-faces t)
 
 ;;;===========================================================================