*** empty log message ***

3 files changed, 37 insertions, 92 deletions

diff --git a/phox/phox-font.el b/phox/phox-font.el
index 8340fb8c..8c0816c9 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -11,94 +11,39 @@
    '("\"\\([^\\\"]\\|\\\\.\\)*\""
     0 'font-lock-string-face t)
     (cons (concat "\\([ \t]\\|^\\)\\("
-       "\\(Cst\\)\\|"
-       "\\(Import\\)\\|"
-       "\\(Use\\)\\|"
-       "\\(Sort\\)\\|"
-       "\\(new_\\(\\(intro\\)\\|\\(elim\\)\\|\\(rewrite\\)\\)\\)\\|"
-       "\\(a\\("
-       (concat
-	"\\(dd_path\\)\\|"
-	"\\(uthor\\)"
-	"\\)\\)\\|")
-       "\\(c\\("
-       (concat
-	"\\(laim\\)\\|"
-	"\\(ose_def\\)\\|"
-	"\\(or\\(ollary\\)?\\)"
-	"\\)\\)\\|")
-       "\\(d\\(\\(e\\(f\\(_thlist\\)?\\|l\\)\\)\\|\\(ocuments\\)\\|\\(epend\\)\\)\\)\\|"
-       "\\(e\\("
-       (concat 
-	"\\(lim_after_intro\\)\\|"
-	"\\(xport\\)\\|"
-	"\\(del\\)\\|"
-	"\\(show\\)"
-	"\\)\\)\\|")
-       "\\(f\\("
-       (concat
-	"\\(act\\)\\|"
-	"\\(lag\\)\\|"
-	"\\)\\)\\|")
-       "\\(goal\\)\\|"
-       "\\(in\\("
-       (concat
-	"\\(clude\\)\\|"
-	"\\(stitute\\)"
-	"\\)\\)\\|")
-       "\\(lem\\(ma\\)?\\)\\|"
-       "\\(p\\("
-       (concat
-	"\\(ath\\)\\|"
-	"\\(r\\("
-	(concat
-	 "\\(int\\(_sort\\)?\\)\\|"
-	 "\\(iority\\)\\|"
-	 "\\(op\\(osition\\)?\\)"
-	 "\\)\\)")
-	"\\)\\)\\|")
-       "\\(quit\\)\\|"
-       "\\(s\\(\\(ave\\)\\|\\(earch\\)\\)\\)\\|"
-       "\\(t\\(" 
-       (concat
-	"\\(ex\\(_syntax\\)?\\)\\|"
-	"\\(eheo\\(rem\\)?\\)\\|"
-	"\\(itle\\)"
-	"\\)\\)")
-       "\\)[ \t.]")
+       "Cst\\|"
+       "Import\\|"
+       "Use\\|"
+       "Sort\\|"
+       "new_\\(intro\\|elim\\|rewrite\\)\\|"
+       "a\\(dd_path\\|uthor\\)\\|"
+       "c\\(laim\\|ose_def\\|or\\(ollary\\)?\\)\\|"
+       "d\\(e\\(f\\(_thlist\\)?\\|l\\)\\|ocuments\\|epend\\)\\|"
+       "e\\(lim_after_intro\\|xport\\|del\\|show\\)\\|"
+       "f\\(act\\|lag\\)\\|"
+       "goal\\|"
+       "in\\(clude\\|stitute\\)\\|"
+       "lem\\(ma\\)?\\|"
+       "p\\(ath\\|r\\(int\\(_sort\\)?\\|iority\\|op\\(osition\\)?\\)\\)\\|"
+       "quit\\|"
+       "s\\(ave\\|earch\\)\\|"
+       "t\\(ex\\(_syntax\\)?\\|eheo\\(rem\\)?\\|itle\\)"
+       "\\)[ \t\n\r.]")
       '(0 'font-lock-keyword-face t))
 ;proof command
     (cons (concat "\\([ \t]\\|^\\)\\("
-       "\\(a\\("
-       (concat
-	"\\(bort\\)\\|"
-	"\\(bsurd\\)\\|"
-	"\\(pply\\)\\|"
-	"\\(xiom\\)"
-	"\\)\\)\\|")
-       "\\(constraints\\)\\|"
-       "\\(elim\\)\\|"
-       "\\(from\\)\\|"
-       "\\(goals\\)\\|"
-       "\\(in\\("
-       (concat
-	"\\(tros?\\)\\|"
-	"\\(stance\\)"
-	"\\)\\)\\|")
-       "\\(l\\("
-       (concat
-	"\\(ocal\\)\\|"
-	"\\(efts?\\)"
-	"\\)\\)\\|")
-       "\\(next\\)\\|"
-       "\\(r\\(\\(ewrite\\(_hyp\\)?\\)\\|\\(ename\\)\\|\\(mh\\)\\)\\)\\|"
-       "\\(slh\\)\\|"
-       "\\(trivial\\)\\|" 
-       "\\(u\\("       
-       (concat
-	"\\(se\\)\\|"
-	"\\(ndo\\)\\|"
-	"\\(nfold\\(_hyp\\)?\\)\\)\\)") 
+       "a\\(b\\(bort\\|surd\\)\\|pply\\|xiom\\)\\|"
+       "constraints\\|"
+       "elim\\|"
+       "from\\|"
+       "goals\\|"
+       "in\\(tros?\\|stance\\)\\|"
+       "l\\(ocal\\|efts?\\)\\|"
+       "next\\|"
+       "r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|"
+       "slh\\|"
+       "trivial\\|" 
+       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\)\\)" 
        "\\)[ \t.]")
       '(0 'font-lock-type-face t))))
 
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 4acaa92d..0e82b1d3 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -33,7 +33,7 @@ send a compile command to PhoX for the theorem which name is under the cursor."
 ; phox-comments-regexp : a sequence of comments and white spaces
  phox-comments-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-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 
diff --git a/phox/phox.el b/phox/phox.el
index b25e46c3..749a8409 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -111,19 +111,19 @@
    proof-comment-start             "(*"
    proof-comment-end               "*)"
    proof-state-command             "goals."
-   proof-goal-command-regexp       "goal\\|\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|fact\\|\\(cor\\(ollary\\)?\\)\\|\\(theo\\(rem\\)?\\)"
+   proof-goal-command-regexp       "goal\\|prop\\(osition\\)?\\|em\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?"
    proof-save-command-regexp       "save"
    proof-goal-with-hole-regexp     (concat 
-     "\\|\\(prop\\(osition\\)?\\)\\|\\(lem\\(ma\\)?\\)\\|fact\\|\\(cor\\(ollary\\)?\\)\\|\\(theo\\(rem\\)?\\)"
+     "\\(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-goal-with-hole-result     13
    proof-save-with-hole-regexp     (concat 
-      "save[ \n\t\r]"
+      "save"
       phox-strict-comments-regexp
       phox-ident-regexp)
-   proof-save-with-hole-result     4
+   proof-save-with-hole-result     8
+   proof-ignore-for-undo-count      "constraints\\|flag\\|goals\\|print\\(_sort\\)?\\|eshow\\|search\\|priority\\|depend"
    proof-shell-error-regexp        "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)"
    proof-non-undoables-regexp      "undo"
    proof-goal-command              "goal %s."