From 961516ffdb286f58a8533c730b789d280c7cd18d Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Tue, 19 Dec 2000 17:16:35 +0000 Subject: *** empty log message *** --- phox/phox-font.el | 5 +++-- phox/phox-fun.el | 5 ++++- phox/phox.el | 12 ++++++------ phox/sym-lock.el | 2 +- 4 files changed, 14 insertions(+), 10 deletions(-) (limited to 'phox') 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) -- cgit v1.2.3