diff options
| -rw-r--r-- | README | 2 | ||||
| -rw-r--r-- | af2/README | 10 | ||||
| -rw-r--r-- | af2/af2-outline.el | 57 | ||||
| -rw-r--r-- | af2/phox-font.el (renamed from af2/af2-font.el) | 14 | ||||
| -rw-r--r-- | af2/phox-fun.el (renamed from af2/af2-fun.el) | 94 | ||||
| -rw-r--r-- | af2/phox-outline.el | 57 | ||||
| -rw-r--r-- | af2/phox-tags.el (renamed from af2/af2-tags.el) | 26 | ||||
| -rw-r--r-- | af2/phox.el (renamed from af2/af2.el) | 174 | ||||
| -rw-r--r-- | generic/proof-site.el | 2 |
9 files changed, 218 insertions, 218 deletions
@@ -26,7 +26,7 @@ For notes on the supported assistants, see the README files in the subdirectories: acl2/ ACL2 - af2/ AF2 + af2/ PhoX coq/ Coq demoisa/ Demonstration instance for Isabelle isa/ Isabelle @@ -1,4 +1,4 @@ -AF2 Proof General, for AF2. +PhoX Proof General, for Phox. Written by Christophe Raffalli @@ -6,13 +6,13 @@ $Id$ Status: supported Maintainer: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> -AF2 version: -AF2 homepage: http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html +PhoX version: 0.7 +PhoX homepage: http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html ======================================== -This mode has support for script management with AF2, and some -other features ported from AF2's own Emacs mode. +This mode has support for script management with PhoX, and some +other features ported from PhoX's own Emacs mode. diff --git a/af2/af2-outline.el b/af2/af2-outline.el deleted file mode 100644 index e3dbf845..00000000 --- a/af2/af2-outline.el +++ /dev/null @@ -1,57 +0,0 @@ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; PARAMÉTRAGE du MODE outline -;;--------------------------------------------------------------------------;; - - -(setq af2-outline-title-regexp "\\((\\*[ \t\n]*title =\\)") -(setq af2-outline-section-regexp "\\((\\*\\*+\\)") -(setq af2-outline-save-regexp "\\((\\*#\\)") -(setq - af2-outline-theo-regexp - "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)") -(setq - af2-outline-theo2-regexp - "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)") - -(setq - af2-outline-regexp - (concat - af2-outline-title-regexp "\\|" - af2-outline-section-regexp "\\|" - af2-outline-save-regexp "\\|" - af2-outline-theo-regexp "\\|" - af2-outline-theo2-regexp)) - -(setq af2-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)") - -;(if af2-outline -; (add-hook 'af2-mode-hook '(lambda()(outline-minor-mode 1))) -; ) - -(defun af2-outline-level() - "Find the level of current outline heading in some af2 libraries." - (let ((retour 0)) - (save-excursion - (cond ((looking-at af2-outline-title-regexp) 1) - ((looking-at af2-outline-section-regexp) - (min 6 (- (match-end 0) (match-beginning 0)))) ; valeur maxi 6 - ((looking-at af2-outline-theo-regexp) 7) - ((looking-at (concat af2-outline-save-regexp "\\|" - af2-outline-theo2-regexp ) - ) 8) - ) - ))) - -(defun af2-setup-outline () - "Set up local variable for outline mode" - (make-local-variable 'outline-heading-end-regexp) - (setq outline-heading-end-regexp af2-outline-heading-end-regexp) - (make-local-variable 'outline-regexp) - (setq outline-regexp af2-outline-regexp) - (make-local-variable 'outline-level) - (setq outline-level 'af2-outline-level) - (outline-minor-mode 1) -) - -(provide 'af2-outline)
\ No newline at end of file diff --git a/af2/af2-font.el b/af2/phox-font.el index 0a67826d..f04844fa 100644 --- a/af2/af2-font.el +++ b/af2/phox-font.el @@ -3,7 +3,7 @@ ;; Font lock keywords ;;--------------------------------------------------------------------------;; -(defconst af2-font-lock-keywords +(defconst phox-font-lock-keywords (list ;commands '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)" @@ -111,7 +111,7 @@ ;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be ;; used to determine the symbol character codes. -(defvar af2-sym-lock-keywords +(defvar phox-sym-lock-keywords '((">=" 0 1 179) ("<=" 0 1 163) ("!=" 0 1 185) @@ -125,14 +125,14 @@ ("-->" 0 1 222) ("->" 0 1 174) ("~" 0 1 216)) - "If non nil: Overrides default Sym-Lock patterns for Af2.") + "If non nil: Overrides default Sym-Lock patterns for PhoX.") -(defun af2-sym-lock-start () - (if (and (featurep 'sym-lock) af2-sym-lock) +(defun phox-sym-lock-start () + (if (and (featurep 'sym-lock) phox-sym-lock) (progn (setq sym-lock-color (face-foreground 'font-lock-function-name-face)) (if (not sym-lock-keywords) - (sym-lock af2-sym-lock-keywords))))) + (sym-lock phox-sym-lock-keywords))))) -(provide 'af2-font) +(provide 'phox-font) diff --git a/af2/af2-fun.el b/af2/phox-fun.el index d03c23ab..58771057 100644 --- a/af2/af2-fun.el +++ b/af2/phox-fun.el @@ -5,15 +5,15 @@ ;; note : program extraction is still experimental ;;--------------------------------------------------------------------------;; -(defun af2-compile-theorem(name) +(defun phox-compile-theorem(name) "Interactive function : -ask for the name of a theorem and send a compile command to af2 for it." +ask for the name of a theorem and send a compile command to PhoX for it." (interactive "stheorem : ") (proof-shell-invisible-command (concat "compile " name ".\n"))) -(defun af2-compile-theorem-around-point() +(defun phox-compile-theorem-around-point() "Interactive function : -send a compile command to af2 for the theorem which name is under the cursor." +send a compile command to PhoX for the theorem which name is under the cursor." (interactive) (let (start end) (save-excursion @@ -21,42 +21,42 @@ send a compile command to af2 for the theorem which name is under the cursor." (setq start (point)) (forward-word -1) (setq end (point))) - (af2-compile-theorem (buffer-substring start end)))) + (phox-compile-theorem (buffer-substring start end)))) (setq - af2-forget-id-command "del %s.\n" - af2-forget-new-elim-command "edel elim %s.\n" - af2-forget-new-intro-command "edel intro %s.\n" - af2-forget-new-rewrite-command "edel rewrite %s.\n" - af2-forget-close-def-command "edel closed %s.\n" - af2-comments-regexp "[ \n\t\r]*\\((\\*\\([^*]\\|\\(\\*[^)]\\)\\)*\\*)[ \n\t\r]*\\)*" - af2-ident-regexp "\\(\\([^ \n\t\r=\\[.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)" - af2-spaces-regexp "[ \n\t\r]*" - af2-sy-definition-regexp (concat + phox-forget-id-command "del %s.\n" + phox-forget-new-elim-command "edel elim %s.\n" + 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 "[ \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\\)" - af2-comments-regexp + phox-comments-regexp "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") - af2-definition-regexp (concat + phox-definition-regexp (concat "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)" - af2-comments-regexp - af2-ident-regexp) - af2-new-elim-regexp (concat + phox-comments-regexp + phox-ident-regexp) + phox-new-elim-regexp (concat "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - af2-ident-regexp) - af2-new-intro-regexp (concat + phox-ident-regexp) + phox-new-intro-regexp (concat "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - af2-ident-regexp) - af2-new-rewrite-regexp (concat + phox-ident-regexp) + phox-new-rewrite-regexp (concat "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - af2-ident-regexp) - af2-close-def-regexp (concat + phox-ident-regexp) + phox-close-def-regexp (concat "close_def" - af2-comments-regexp + phox-comments-regexp "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]") ) -(defun af2-find-and-forget (span) +(defun phox-find-and-forget (span) (let (str ans tmp (lsp -1)) (while span (setq str (span-property span 'cmd)) @@ -66,36 +66,36 @@ send a compile command to af2 for the theorem which name is under the cursor." ((eq (span-property span 'type) 'comment)) ((eq (span-property span 'type) 'goalsave) - (setq ans (concat (format af2-forget-id-command + (setq ans (concat (format phox-forget-id-command (span-property span 'name)) ans))) - ((proof-string-match af2-new-elim-regexp str) + ((proof-string-match phox-new-elim-regexp str) (setq ans - (concat (format af2-forget-new-elim-command + (concat (format phox-forget-new-elim-command (match-string 3 str)) ans))) - ((proof-string-match af2-new-intro-regexp str) + ((proof-string-match phox-new-intro-regexp str) (setq ans - (concat (format af2-forget-new-intro-command + (concat (format phox-forget-new-intro-command (match-string 3 str)) ans))) - ((proof-string-match af2-new-rewrite-regexp str) + ((proof-string-match phox-new-rewrite-regexp str) (setq ans - (concat (format af2-forget-new-rewrite-command + (concat (format phox-forget-new-rewrite-command (match-string 3 str)) ans))) - ((proof-string-match af2-close-def-regexp str) + ((proof-string-match phox-close-def-regexp str) (setq ans - (concat (format af2-forget-close-def-command + (concat (format phox-forget-close-def-command (match-string 4 str)) ans))) - ((proof-string-match af2-sy-definition-regexp str) + ((proof-string-match phox-sy-definition-regexp str) (setq ans - (concat (format af2-forget-id-command + (concat (format phox-forget-id-command (concat "$" (match-string 7 str))) ans))) - ((proof-string-match af2-definition-regexp str) - (setq ans (concat (format af2-forget-id-command + ((proof-string-match phox-definition-regexp str) + (setq ans (concat (format phox-forget-id-command (match-string 6 str)) ans)))) @@ -111,15 +111,15 @@ send a compile command to af2 for the theorem which name is under the cursor." ;;--------------------------------------------------------------------------;; -(defun af2-delete-symbol(symbol) +(defun phox-delete-symbol(symbol) "Interactive function : -ask for a symbol and send a delete command to af2 for it." +ask for a symbol and send a delete command to PhoX for it." (interactive "ssymbol : ") (proof-shell-invisible-command (concat "del " symbol ".\n"))) -(defun af2-delete-symbol-around-point() +(defun phox-delete-symbol-around-point() "Interactive function : -send a delete command to af2 for the symbol whose name is under the cursor." +send a delete command to PhoX for the symbol whose name is under the cursor." (interactive) (let (start end) (save-excursion @@ -128,13 +128,13 @@ send a delete command to af2 for the symbol whose name is under the cursor." (forward-word 1) (setq end (point))) (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) - (af2-delete-symbol (buffer-substring start end)))) + (phox-delete-symbol (buffer-substring start end)))) ;; ;; Doing commands ;; -(defun af2-assert-next-command-interactive () +(defun phox-assert-next-command-interactive () "Process until the end of the next unprocessed command after point. If inside a comment, just process until the start of the comment." (interactive) @@ -146,5 +146,5 @@ If inside a comment, just process until the start of the comment." (proof-assert-next-command)) (proof-maybe-follow-locked-end))) -(provide 'af2-fun) +(provide 'phox-fun) diff --git a/af2/phox-outline.el b/af2/phox-outline.el new file mode 100644 index 00000000..766bddb3 --- /dev/null +++ b/af2/phox-outline.el @@ -0,0 +1,57 @@ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; PARAMÉTRAGE du MODE outline +;;--------------------------------------------------------------------------;; + + +(setq phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)") +(setq phox-outline-section-regexp "\\((\\*\\*+\\)") +(setq phox-outline-save-regexp "\\((\\*#\\)") +(setq + phox-outline-theo-regexp + "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)") +(setq + phox-outline-theo2-regexp + "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)") + +(setq + phox-outline-regexp + (concat + phox-outline-title-regexp "\\|" + phox-outline-section-regexp "\\|" + phox-outline-save-regexp "\\|" + phox-outline-theo-regexp "\\|" + phox-outline-theo2-regexp)) + +(setq phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)") + +;(if phox-outline +; (add-hook 'phox-mode-hook '(lambda()(outline-minor-mode 1))) +; ) + +(defun phox-outline-level() + "Find the level of current outline heading in some PhoX libraries." + (let ((retour 0)) + (save-excursion + (cond ((looking-at phox-outline-title-regexp) 1) + ((looking-at phox-outline-section-regexp) + (min 6 (- (match-end 0) (match-beginning 0)))) ; valeur maxi 6 + ((looking-at phox-outline-theo-regexp) 7) + ((looking-at (concat phox-outline-save-regexp "\\|" + phox-outline-theo2-regexp ) + ) 8) + ) + ))) + +(defun phox-setup-outline () + "Set up local variable for outline mode" + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp phox-outline-heading-end-regexp) + (make-local-variable 'outline-regexp) + (setq outline-regexp phox-outline-regexp) + (make-local-variable 'outline-level) + (setq outline-level 'phox-outline-level) + (outline-minor-mode 1) +) + +(provide 'phox-outline)
\ No newline at end of file diff --git a/af2/af2-tags.el b/af2/phox-tags.el index 1c60b631..f2b5959a 100644 --- a/af2/af2-tags.el +++ b/af2/phox-tags.el @@ -15,7 +15,7 @@ (require 'etags) -(defun af2-tags-add-table(table) +(defun phox-tags-add-table(table) "add tags table" (interactive "D directory, location of a file named TAGS to add : ") (if proof-running-on-XEmacs @@ -32,7 +32,7 @@ ) ) -(defun af2-tags-reset-table() +(defun phox-tags-reset-table() "Set tags-table-list to nil." (interactive) ; (make-local-variable 'tags-table-list) @@ -42,28 +42,28 @@ (setq tags-table-list nil)) ) -(defun af2-tags-add-doc-table() +(defun phox-tags-add-doc-table() "Add tags in text documentation." (interactive) - (af2-tags-add-table (concat af2-doc-dir "/text/TAGS")) + (phox-tags-add-table (concat phox-doc-dir "/text/TAGS")) ) -(defun af2-tags-add-lib-table() +(defun phox-tags-add-lib-table() "Add tags in libraries." (interactive) - (af2-tags-add-table (concat af2-lib-dir "TAGS")) + (phox-tags-add-table (concat phox-lib-dir "TAGS")) ) -(defun af2-tags-add-local-table() - "Add the tags table created with function af2-create-local-table." +(defun phox-tags-add-local-table() + "Add the tags table created with function phox-create-local-table." (interactive) - (af2-tags-add-table (concat buffer-file-name "TAGS")) + (phox-tags-add-table (concat buffer-file-name "TAGS")) ) -(defun af2-tags-create-local-table() +(defun phox-tags-create-local-table() "create table on local buffer" (interactive) - (shell-command (concat af2-etags + (shell-command (concat phox-etags " -o " (file-name-nondirectory (buffer-file-name)) "TAGS " @@ -72,6 +72,6 @@ ;; default -(if af2-tags-doc (add-hook 'af2-mode-hook 'af2-tags-add-doc-table)) +(if phox-tags-doc (add-hook 'phox-mode-hook 'phox-tags-add-doc-table)) -(provide 'af2-tags)
\ No newline at end of file +(provide 'phox-tags)
\ No newline at end of file diff --git a/af2/af2.el b/af2/phox.el index 38f423cf..49f4ab15 100644 --- a/af2/af2.el +++ b/af2/phox.el @@ -3,11 +3,11 @@ ;; Adjust toolbar entries. (Must be done ;; before proof-toolbar is loaded). -(if proof-running-on-XEmacs (setq af2-toolbar-entries - (remassoc 'context af2-toolbar-entries))) +(if proof-running-on-XEmacs (setq phox-toolbar-entries + (remassoc 'context phox-toolbar-entries))) -;; ======== User settings for Af2 ======== +;; ======== User settings for PhoX ======== ;; ;; Defining variables using customize is pretty easy. ;; You should do it at least for your prover-specific user options. @@ -15,84 +15,84 @@ ;; proof-site provides us with two customization groups ;; automatically: (based on the name of the assistant) ;; -;; 'af2 - User options for Af2 Proof General -;; 'af2-config - Configuration of Af2 Proof General +;; 'phox - User options for PhoX Proof General +;; 'phox-config - Configuration of PhoX Proof General ;; (constants, but may be nice to tweak) ;; ;; The first group appears in the menu -;; ProofGeneral -> Customize -> Af2 +;; ProofGeneral -> Customize -> PhoX ;; The second group appears in the menu: -;; ProofGeneral -> Internals -> Af2 config +;; ProofGeneral -> Internals -> PhoX config ;; -(defcustom af2-prog-name "af2 -pg" - "*Name of program to run Af2." +(defcustom phox-prog-name "phox -pg" + "*Name of program to run PhoX." :type 'file - :group 'af2) + :group 'phox) -(defcustom af2-sym-lock t +(defcustom phox-sym-lock t "*Whether to use sym-lock or not." :type 'boolean - :group 'af2) + :group 'phox) -(defcustom af2-web-page - "http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html" - "URL of web page for Af2." +(defcustom phox-web-page + "http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html" + "URL of web page for PhoX." :type 'string - :group 'af2-config) + :group 'phox-config) -(defcustom af2-doc-dir - "/usr/local/doc/af2" - "The name of the root documentation directory for af2." +(defcustom phox-doc-dir + "/usr/local/doc/phox" + "The name of the root documentation directory for PhoX." :type 'string - :group 'af2-config) + :group 'phox-config) -(defcustom af2-lib-dir - "/usr/local/lib/af2" - "The name of the root directory for af2 libraries." +(defcustom phox-lib-dir + "/usr/local/lib/phox" + "The name of the root directory for PhoX libraries." :type 'string - :group 'af2-config) + :group 'phox-config) -(defcustom af2-tags-program - (concat af2-doc-dir "/tools/af2_etags.sh") +(defcustom phox-tags-program + (concat phox-doc-dir "/tools/phox_etags.sh") "Program to run to generate TAGS table for proof assistant." :type 'string - :group 'af2-config) + :group 'phox-config) -(defcustom af2-tags-doc +(defcustom phox-tags-doc t - "*If non nil, tags table for af2 text documentation is loaded." + "*If non nil, tags table for PhoX text documentation is loaded." :type 'boolean - :group 'af2-config) + :group 'phox-config) -(defcustom af2-etags - (concat af2-doc-dir "/tools/af2_etags.sh") +(defcustom phox-etags + (concat phox-doc-dir "/tools/phox_etags.sh") "Command to build tags table." :type 'string - :group 'af2-config) + :group 'phox-config) -(require 'af2-tags) -(require 'af2-outline) -(require 'af2-font) -(require 'af2-fun) +(require 'phox-tags) +(require 'phox-outline) +(require 'phox-font) +(require 'phox-fun) -;; ----- Af2 specific menu +;; ----- PhoX specific menu (defpgdefault menu-entries '( - ["Delete symbol around cursor" af2-delete-symbol-around-point t] - ["Delete symbol" af2-delete-symbol t] - ["Compile theorem under cursor" af2-compile-theorem-around-point t] + ["Delete symbol around cursor" phox-delete-symbol-around-point t] + ["Delete symbol" phox-delete-symbol t] + ["Compile theorem under cursor" phox-compile-theorem-around-point t] "----" ("Tags" - ["create a tags table for local buffer" af2-tags-create-local-table t] + ["create a tags table for local buffer" phox-tags-create-local-table t] ["------------------" nil nil] -; ["load table" af2-tags-load-table t] - ["add table" af2-tags-add-table t] - ["add local table" af2-tags-add-local-table t] - ["add table for libraries" af2-tags-add-lib-table t] - ["add table for text doc" af2-tags-add-doc-table t] - ["reset tags table list" af2-tags-reset-table t] +; ["load table" phox-tags-load-table t] + ["add table" phox-tags-add-table t] + ["add local table" phox-tags-add-local-table t] + ["add table for libraries" phox-tags-add-lib-table t] + ["add table for text doc" phox-tags-add-doc-table t] + ["reset tags table list" phox-tags-reset-table t] ["------------------" nil nil] ["Find theorem, definition ..." find-tag t] ["complete theorem, definition ..." complete-tag t] @@ -103,8 +103,8 @@ ;; ======== Configuration of generic modes ======== ;; -(defun af2-config () - "Configure Proof General scripting for Af2." +(defun phox-config () + "Configure Proof General scripting for PhoX." (setq proof-terminal-char ?\. ; ends every command proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" @@ -115,14 +115,14 @@ proof-save-command-regexp "save" proof-goal-with-hole-regexp (concat "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)" - af2-comments-regexp - af2-ident-regexp) + phox-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" - af2-comments-regexp - af2-ident-regexp) + phox-comments-regexp + phox-ident-regexp) proof-save-with-hole-result 4 proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror" proof-non-undoables-regexp "undo" @@ -131,19 +131,19 @@ proof-kill-goal-command "abort." proof-showproof-command "goals." proof-undo-n-times-cmd "undo %s." - proof-find-and-forget-fn 'af2-find-and-forget + proof-find-and-forget-fn 'phox-find-and-forget proof-find-theorems-command "search \"%s\"." proof-auto-multiple-files nil - font-lock-keywords af2-font-lock-keywords + font-lock-keywords phox-font-lock-keywords ) ) -(defun af2-shell-config () - "Configure Proof General shell for Af2." +(defun phox-shell-config () + "Configure Proof General shell for PhoX." (setq ;proof-shell-cd-cmd "cd \"%s\"" - proof-shell-prompt-pattern "\\(>af2> \\)\\|\\(%af2% \\)" - proof-shell-annotated-prompt-regexp "\\(>af2> \\)\\|\\(%af2% \\)" + proof-shell-prompt-pattern "\\(>phox> \\)\\|\\(%phox% \\)" + proof-shell-annotated-prompt-regexp "\\(>phox> \\)\\|\\(%phox% \\)" proof-shell-interrupt-regexp "Interrupt" proof-shell-start-goals-regexp "^Goals left to prove:" proof-shell-quit-cmd "quit." @@ -162,44 +162,44 @@ ;; The derived modes set the variables, then call the ;; <mode>-config-done function to complete configuration. -(define-derived-mode af2-mode proof-mode - "Af2 script" nil - (af2-config) - (af2-sym-lock-start) +(define-derived-mode phox-mode proof-mode + "PhoX script" nil + (phox-config) + (phox-sym-lock-start) (proof-config-done) - (af2-setup-outline) - (define-key af2-mode-map [(control j)] - 'af2-assert-next-command-interactive) + (phox-setup-outline) + (define-key phox-mode-map [(control j)] + 'phox-assert-next-command-interactive) ;; with the previous binding, ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed" - (define-key af2-mode-map [(control c) (meta d)] - 'af2-delete-symbol-around-point) + (define-key phox-mode-map [(control c) (meta d)] + 'phox-delete-symbol-around-point) ;; Configure syntax table for block comments (modify-syntax-entry ?\* ". 23") (modify-syntax-entry ?\( "()1") (modify-syntax-entry ?\) ")(4")) -(define-derived-mode af2-shell-mode proof-shell-mode - "Af2 shell" nil - (af2-shell-config) +(define-derived-mode phox-shell-mode proof-shell-mode + "PhoX shell" nil + (phox-shell-config) (proof-shell-config-done)) -(define-derived-mode af2-response-mode proof-response-mode - "Af2 response" nil +(define-derived-mode phox-response-mode proof-response-mode + "PhoX response" nil (setq - font-lock-keywords af2-font-lock-keywords + font-lock-keywords phox-font-lock-keywords proof-output-fontify-enable t) - (af2-sym-lock-start) + (phox-sym-lock-start) (proof-response-config-done) (font-lock-mode)) -(define-derived-mode af2-goals-mode proof-goals-mode - "Af2 goals" nil +(define-derived-mode phox-goals-mode proof-goals-mode + "PhoX goals" nil (setq - font-lock-keywords af2-font-lock-keywords + font-lock-keywords phox-font-lock-keywords proof-output-fontify-enable t) - (af2-sym-lock-start) + (phox-sym-lock-start) (proof-goals-config-done) (font-lock-mode)) @@ -216,14 +216,14 @@ ;; name of the program to run, and the modes for the shell, response, ;; and goals buffers. -(add-hook 'proof-pre-shell-start-hook 'af2-pre-shell-start) +(add-hook 'proof-pre-shell-start-hook 'phox-pre-shell-start) -(defun af2-pre-shell-start () - (setq proof-prog-name af2-prog-name) - (setq proof-mode-for-shell 'af2-shell-mode) - (setq proof-mode-for-response 'af2-response-mode) - (setq proof-mode-for-goals 'af2-goals-mode)) +(defun phox-pre-shell-start () + (setq proof-prog-name phox-prog-name) + (setq proof-mode-for-shell 'phox-shell-mode) + (setq proof-mode-for-response 'phox-response-mode) + (setq proof-mode-for-goals 'phox-goals-mode)) -(provide 'af2) +(provide 'phox) diff --git a/generic/proof-site.el b/generic/proof-site.el index 3ddc2da4..84e91497 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -48,7 +48,7 @@ (isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$") - (af2 "Af2" "\\.af2$") + (phox "PhoX" "\\.phx$") ;; The following provers are not fully supported, ;; and have only preliminary support written ;; (please volunteer to improve them!) |