*** empty log message ***

4 files changed, 14 insertions, 10 deletions

diff --git a/phox/phox-font.el b/phox/phox-font.el
index f04844fa..8340fb8c 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -107,7 +107,7 @@
 ;;                       Sym-lock tables
 ;;--------------------------------------------------------------------------;;
 
-(if proof-running-on-XEmacs (require 'sym-lock))
+(if proof-running-on-XEmacs (require 'phox-sym-lock))
 
 ;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be
 ;; used to determine the symbol character codes.
@@ -124,7 +124,8 @@
     ("<->" 0 1 171)
     ("-->" 0 1 222)
     ("->" 0 1 174)
-    ("~" 0 1 216))
+    ("~" 0 1 216)
+    ("\\\\" 0 1 108))
   "If non nil: Overrides default Sym-Lock patterns for PhoX.")
 
 (defun phox-sym-lock-start ()
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 58771057..4acaa92d 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -30,8 +30,11 @@ send a compile command to PhoX for the theorem which name is under the cursor."
  phox-forget-new-intro-command "edel intro %s.\n"
  phox-forget-new-rewrite-command "edel rewrite %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]*\\)*"
- phox-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)"
+; phox-strict-comments-regexp : a not empty sequence of comments and white spaces
+ phox-strict-comments-regexp "\\([ \n\t\r]+\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*\\)\\|\\(\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)+\\)"
+ phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)"
  phox-spaces-regexp "[ \n\t\r]*"
  phox-sy-definition-regexp (concat 
    "\\(Cst\\|def\\)"
diff --git a/phox/phox.el b/phox/phox.el
index 49f4ab15..b25e46c3 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -111,20 +111,20 @@
    proof-comment-start             "(*"
    proof-comment-end               "*)"
    proof-state-command             "goals."
-   proof-goal-command-regexp       "goal\\|prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem"
+   proof-goal-command-regexp       "goal\\|\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|fact\\|\\(cor\\(ollary\\)?\\)\\|\\(theo\\(rem\\)?\\)"
    proof-save-command-regexp       "save"
    proof-goal-with-hole-regexp     (concat 
-      "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)"
-      phox-comments-regexp
+     "\\|\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|fact\\|\\(cor\\(ollary\\)?\\)\\|\\(theo\\(rem\\)?\\)"
+      phox-strict-comments-regexp
       phox-ident-regexp)
    proof-ignore-for-undo-count      "constraints\\|flags\\|goals\\|print\\|print_sort\\|eshow\\|search\\|priority\\|depend"
    proof-goal-with-hole-result     5
    proof-save-with-hole-regexp     (concat 
-      "save"
-      phox-comments-regexp
+      "save[ \n\t\r]"
+      phox-strict-comments-regexp
       phox-ident-regexp)
    proof-save-with-hole-result     4
-   proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror"
+   proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)"
    proof-non-undoables-regexp      "undo"
    proof-goal-command              "goal %s."
    proof-save-command              "save %s."
diff --git a/phox/sym-lock.el b/phox/sym-lock.el
index 085ef268..3763676b 100644
--- a/phox/sym-lock.el
+++ b/phox/sym-lock.el
@@ -306,4 +306,4 @@ OBJ under `sym-lock-adobe-symbol-face'. The face extent will become atomic."
 
 (add-hook 'font-lock-mode-hook 'sym-lock-font-lock-hook)
 
-(provide 'sym-lock)
+(provide 'phox-sym-lock)