1 files changed, 30 insertions, 85 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))))