From aa7e179bbda6806ca6af1f0726d891dd1f71c6df Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Thu, 21 Dec 2000 16:04:21 +0000 Subject: *** empty log message *** --- phox/phox-font.el | 115 ++++++++++++++---------------------------------------- phox/phox-fun.el | 2 +- phox/phox.el | 12 +++--- 3 files changed, 37 insertions(+), 92 deletions(-) (limited to 'phox') 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." -- cgit v1.2.3