From bf35167a87fc74a3317b2c08937b85e4b48cf0d0 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Fri, 1 Dec 2000 17:32:21 +0000 Subject: af2 is now called PhoX --- README | 2 +- af2/README | 10 +-- af2/af2-font.el | 138 ------------------------------ af2/af2-fun.el | 150 --------------------------------- af2/af2-outline.el | 57 ------------- af2/af2-tags.el | 77 ----------------- af2/af2.el | 229 -------------------------------------------------- af2/phox-font.el | 138 ++++++++++++++++++++++++++++++ af2/phox-fun.el | 150 +++++++++++++++++++++++++++++++++ af2/phox-outline.el | 57 +++++++++++++ af2/phox-tags.el | 77 +++++++++++++++++ af2/phox.el | 229 ++++++++++++++++++++++++++++++++++++++++++++++++++ generic/proof-site.el | 2 +- 13 files changed, 658 insertions(+), 658 deletions(-) delete mode 100644 af2/af2-font.el delete mode 100644 af2/af2-fun.el delete mode 100644 af2/af2-outline.el delete mode 100644 af2/af2-tags.el delete mode 100644 af2/af2.el create mode 100644 af2/phox-font.el create mode 100644 af2/phox-fun.el create mode 100644 af2/phox-outline.el create mode 100644 af2/phox-tags.el create mode 100644 af2/phox.el diff --git a/README b/README index bb381ac0..ba42bc4a 100644 --- a/README +++ b/README @@ -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 diff --git a/af2/README b/af2/README index 8d0f990f..9c955b84 100644 --- a/af2/README +++ b/af2/README @@ -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 -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-font.el b/af2/af2-font.el deleted file mode 100644 index 0a67826d..00000000 --- a/af2/af2-font.el +++ /dev/null @@ -1,138 +0,0 @@ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; Font lock keywords -;;--------------------------------------------------------------------------;; - -(defconst af2-font-lock-keywords - (list -;commands - '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)" - 0 'font-lock-comment-face t) - '("\"\\([^\\\"]\\|\\\\.\\)*\"" - 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.]") - '(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\\)?\\)\\)\\)") - "\\)[ \t.]") - '(0 'font-lock-type-face t)))) - -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; Sym-lock tables -;;--------------------------------------------------------------------------;; - -(if proof-running-on-XEmacs (require 'sym-lock)) - -;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be -;; used to determine the symbol character codes. -(defvar af2-sym-lock-keywords - '((">=" 0 1 179) - ("<=" 0 1 163) - ("!=" 0 1 185) - (":<" 0 1 206) - ("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206) - ("\\\\/" 0 1 36) - ("/\\\\" 0 1 34) - ("\\" 0 3 218) - ("&" 0 1 217) - ("<->" 0 1 171) - ("-->" 0 1 222) - ("->" 0 1 174) - ("~" 0 1 216)) - "If non nil: Overrides default Sym-Lock patterns for Af2.") - -(defun af2-sym-lock-start () - (if (and (featurep 'sym-lock) af2-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))))) - -(provide 'af2-font) diff --git a/af2/af2-fun.el b/af2/af2-fun.el deleted file mode 100644 index d03c23ab..00000000 --- a/af2/af2-fun.el +++ /dev/null @@ -1,150 +0,0 @@ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; program extraction. -;; -;; note : program extraction is still experimental -;;--------------------------------------------------------------------------;; - -(defun af2-compile-theorem(name) - "Interactive function : -ask for the name of a theorem and send a compile command to af2 for it." - (interactive "stheorem : ") - (proof-shell-invisible-command (concat "compile " name ".\n"))) - -(defun af2-compile-theorem-around-point() -"Interactive function : -send a compile command to af2 for the theorem which name is under the cursor." - (interactive) - (let (start end) - (save-excursion - (forward-word 1) - (setq start (point)) - (forward-word -1) - (setq end (point))) - (af2-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 - "\\(Cst\\|def\\)" - af2-comments-regexp - "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") - af2-definition-regexp (concat - "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)" - af2-comments-regexp - af2-ident-regexp) - af2-new-elim-regexp (concat - "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - af2-ident-regexp) - af2-new-intro-regexp (concat - "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - af2-ident-regexp) - af2-new-rewrite-regexp (concat - "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" - af2-ident-regexp) - af2-close-def-regexp (concat - "close_def" - af2-comments-regexp - "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]") -) - -(defun af2-find-and-forget (span) - (let (str ans tmp (lsp -1)) - (while span - (setq str (span-property span 'cmd)) - - (cond - - ((eq (span-property span 'type) 'comment)) - - ((eq (span-property span 'type) 'goalsave) - (setq ans (concat (format af2-forget-id-command - (span-property span 'name)) ans))) - - ((proof-string-match af2-new-elim-regexp str) - (setq ans - (concat (format af2-forget-new-elim-command - (match-string 3 str)) ans))) - - ((proof-string-match af2-new-intro-regexp str) - (setq ans - (concat (format af2-forget-new-intro-command - (match-string 3 str)) ans))) - - ((proof-string-match af2-new-rewrite-regexp str) - (setq ans - (concat (format af2-forget-new-rewrite-command - (match-string 3 str)) ans))) - - ((proof-string-match af2-close-def-regexp str) - (setq ans - (concat (format af2-forget-close-def-command - (match-string 4 str)) ans))) - - ((proof-string-match af2-sy-definition-regexp str) - (setq ans - (concat (format af2-forget-id-command - (concat "$" (match-string 7 str))) ans))) - - ((proof-string-match af2-definition-regexp str) - (setq ans (concat (format af2-forget-id-command - (match-string 6 str)) ans)))) - - - (setq lsp (span-start span)) - (setq span (next-span span 'type))) - - (or ans proof-no-command))) - -;;--------------------------------------------------------------------------;; -;; -;; Deleting symbols -;; -;;--------------------------------------------------------------------------;; - - -(defun af2-delete-symbol(symbol) - "Interactive function : -ask for a symbol and send a delete command to af2 for it." - (interactive "ssymbol : ") - (proof-shell-invisible-command (concat "del " symbol ".\n"))) - -(defun af2-delete-symbol-around-point() -"Interactive function : -send a delete command to af2 for the symbol whose name is under the cursor." - (interactive) - (let (start end) - (save-excursion - (forward-word -1) - (setq start (point)) - (forward-word 1) - (setq end (point))) - (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) - (af2-delete-symbol (buffer-substring start end)))) - -;; -;; Doing commands -;; - -(defun af2-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) - (message "test") - (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n")) - (proof-with-script-buffer - (proof-maybe-save-point - (goto-char (proof-queue-or-locked-end)) - (proof-assert-next-command)) - (proof-maybe-follow-locked-end))) - -(provide 'af2-fun) - 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-tags.el b/af2/af2-tags.el deleted file mode 100644 index 1c60b631..00000000 --- a/af2/af2-tags.el +++ /dev/null @@ -1,77 +0,0 @@ -;;--------------------------------------------------------------------------;; -;;--------------------------------------------------------------------------;; -;; gestion des TAGS -;;--------------------------------------------------------------------------;; - -; sous xemacs, visit-tags-table n'a pas d'argument optionnel. Sous gnu emacs : - -; Normally M-x visit-tags-table sets the global value of `tags-file-name'. -; With a prefix arg, set the buffer-local value instead. - -; mieux vaut sous gnu emacs gérer la variable tags-table-list, qui -; n'existe pas sous xemacs. -; Sous xemacs il faut gérer la variable tag-table-alist qui n'existe pas -; sous gnu emacs. - -(require 'etags) - -(defun af2-tags-add-table(table) - "add tags table" - (interactive "D directory, location of a file named TAGS to add : ") - (if proof-running-on-XEmacs - (let ((association (cons buffer-file-name table))) - (if (member association tag-table-alist) - (message (concat table " already loaded.")) - (setq tag-table-alist (cons association tag-table-alist)))) - ; gnu emacs - (if (member table tags-table-list) - (message (concat table " already loaded.")) -; (make-local-variable 'tags-table-list) ; ne focntionne pas - (setq tags-table-list (cons table tags-table-list)) - ) - ) - ) - -(defun af2-tags-reset-table() - "Set tags-table-list to nil." - (interactive) -; (make-local-variable 'tags-table-list) - (if proof-running-on-XEmacs - (progn - (setq tag-table-alist (remassoc buffer-file-name tag-table-alist))) - (setq tags-table-list nil)) - ) - -(defun af2-tags-add-doc-table() - "Add tags in text documentation." - (interactive) - (af2-tags-add-table (concat af2-doc-dir "/text/TAGS")) - ) - -(defun af2-tags-add-lib-table() - "Add tags in libraries." - (interactive) - (af2-tags-add-table (concat af2-lib-dir "TAGS")) - ) - -(defun af2-tags-add-local-table() - "Add the tags table created with function af2-create-local-table." - (interactive) - (af2-tags-add-table (concat buffer-file-name "TAGS")) - ) - -(defun af2-tags-create-local-table() - "create table on local buffer" - (interactive) - (shell-command (concat af2-etags - " -o " - (file-name-nondirectory (buffer-file-name)) - "TAGS " - (file-name-nondirectory (buffer-file-name)))) - ) - -;; default - -(if af2-tags-doc (add-hook 'af2-mode-hook 'af2-tags-add-doc-table)) - -(provide 'af2-tags) \ No newline at end of file diff --git a/af2/af2.el b/af2/af2.el deleted file mode 100644 index 38f423cf..00000000 --- a/af2/af2.el +++ /dev/null @@ -1,229 +0,0 @@ -(require 'proof) ; load generic parts - -;; 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))) - - -;; ======== User settings for Af2 ======== -;; -;; Defining variables using customize is pretty easy. -;; You should do it at least for your prover-specific user options. -;; -;; 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 -;; (constants, but may be nice to tweak) -;; -;; The first group appears in the menu -;; ProofGeneral -> Customize -> Af2 -;; The second group appears in the menu: -;; ProofGeneral -> Internals -> Af2 config -;; - -(defcustom af2-prog-name "af2 -pg" - "*Name of program to run Af2." - :type 'file - :group 'af2) - -(defcustom af2-sym-lock t - "*Whether to use sym-lock or not." - :type 'boolean - :group 'af2) - -(defcustom af2-web-page - "http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html" - "URL of web page for Af2." - :type 'string - :group 'af2-config) - -(defcustom af2-doc-dir - "/usr/local/doc/af2" - "The name of the root documentation directory for af2." - :type 'string - :group 'af2-config) - -(defcustom af2-lib-dir - "/usr/local/lib/af2" - "The name of the root directory for af2 libraries." - :type 'string - :group 'af2-config) - -(defcustom af2-tags-program - (concat af2-doc-dir "/tools/af2_etags.sh") - "Program to run to generate TAGS table for proof assistant." - :type 'string - :group 'af2-config) - -(defcustom af2-tags-doc - t - "*If non nil, tags table for af2 text documentation is loaded." - :type 'boolean - :group 'af2-config) - -(defcustom af2-etags - (concat af2-doc-dir "/tools/af2_etags.sh") - "Command to build tags table." - :type 'string - :group 'af2-config) - -(require 'af2-tags) -(require 'af2-outline) -(require 'af2-font) -(require 'af2-fun) - -;; ----- Af2 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] - "----" - ("Tags" - ["create a tags table for local buffer" af2-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] - ["------------------" nil nil] - ["Find theorem, definition ..." find-tag t] - ["complete theorem, definition ..." complete-tag t] - ) - )) - -;; -;; ======== Configuration of generic modes ======== -;; - -(defun af2-config () - "Configure Proof General scripting for Af2." - (setq - proof-terminal-char ?\. ; ends every command - proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" - 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-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) - 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) - proof-save-with-hole-result 4 - proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(e\\|E\\)rror" - proof-non-undoables-regexp "undo" - proof-goal-command "goal %s." - proof-save-command "save %s." - 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-theorems-command "search \"%s\"." - proof-auto-multiple-files nil - font-lock-keywords af2-font-lock-keywords - ) -) - -(defun af2-shell-config () - "Configure Proof General shell for Af2." - (setq - ;proof-shell-cd-cmd "cd \"%s\"" - proof-shell-prompt-pattern "\\(>af2> \\)\\|\\(%af2% \\)" - proof-shell-annotated-prompt-regexp "\\(>af2> \\)\\|\\(%af2% \\)" - proof-shell-interrupt-regexp "Interrupt" - proof-shell-start-goals-regexp "^Goals left to prove:" - proof-shell-quit-cmd "quit." - proof-shell-restart-cmd "quit." - proof-shell-proof-completed-regexp "^.*^proved" -)) - - -;; -;; ======== Defining the derived modes ======== -;; - -;; The name of the script mode is always -script, -;; but the others can be whatever you like. -;; -;; The derived modes set the variables, then call the -;; -config-done function to complete configuration. - -(define-derived-mode af2-mode proof-mode - "Af2 script" nil - (af2-config) - (af2-sym-lock-start) - (proof-config-done) - (af2-setup-outline) - (define-key af2-mode-map [(control j)] - 'af2-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) - ;; 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) - (proof-shell-config-done)) - -(define-derived-mode af2-response-mode proof-response-mode - "Af2 response" nil - (setq - font-lock-keywords af2-font-lock-keywords - proof-output-fontify-enable t) - (af2-sym-lock-start) - (proof-response-config-done) - (font-lock-mode)) - -(define-derived-mode af2-goals-mode proof-goals-mode - "Af2 goals" nil - (setq - font-lock-keywords af2-font-lock-keywords - proof-output-fontify-enable t) - (af2-sym-lock-start) - (proof-goals-config-done) - (font-lock-mode)) - -;; The response buffer and goals buffer modes defined above are -;; trivial. In fact, we don't need to define them at all -- they -;; would simply default to "proof-response-mode" and "pbp-mode". - -;; A more sophisticated instantiation might set font-lock-keywords to -;; add highlighting, or some of the proof by pointing markup -;; configuration for the goals buffer. - -;; The final piece of magic here is a hook which configures settings -;; to get the proof shell running. Proof General needs to know the -;; 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) - -(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)) - -(provide 'af2) - - diff --git a/af2/phox-font.el b/af2/phox-font.el new file mode 100644 index 00000000..f04844fa --- /dev/null +++ b/af2/phox-font.el @@ -0,0 +1,138 @@ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; Font lock keywords +;;--------------------------------------------------------------------------;; + +(defconst phox-font-lock-keywords + (list +;commands + '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)" + 0 'font-lock-comment-face t) + '("\"\\([^\\\"]\\|\\\\.\\)*\"" + 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.]") + '(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\\)?\\)\\)\\)") + "\\)[ \t.]") + '(0 'font-lock-type-face t)))) + +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; Sym-lock tables +;;--------------------------------------------------------------------------;; + +(if proof-running-on-XEmacs (require 'sym-lock)) + +;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be +;; used to determine the symbol character codes. +(defvar phox-sym-lock-keywords + '((">=" 0 1 179) + ("<=" 0 1 163) + ("!=" 0 1 185) + (":<" 0 1 206) + ("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206) + ("\\\\/" 0 1 36) + ("/\\\\" 0 1 34) + ("\\" 0 3 218) + ("&" 0 1 217) + ("<->" 0 1 171) + ("-->" 0 1 222) + ("->" 0 1 174) + ("~" 0 1 216)) + "If non nil: Overrides default Sym-Lock patterns for PhoX.") + +(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 phox-sym-lock-keywords))))) + +(provide 'phox-font) diff --git a/af2/phox-fun.el b/af2/phox-fun.el new file mode 100644 index 00000000..58771057 --- /dev/null +++ b/af2/phox-fun.el @@ -0,0 +1,150 @@ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; program extraction. +;; +;; note : program extraction is still experimental +;;--------------------------------------------------------------------------;; + +(defun phox-compile-theorem(name) + "Interactive function : +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 phox-compile-theorem-around-point() +"Interactive function : +send a compile command to PhoX for the theorem which name is under the cursor." + (interactive) + (let (start end) + (save-excursion + (forward-word 1) + (setq start (point)) + (forward-word -1) + (setq end (point))) + (phox-compile-theorem (buffer-substring start end)))) + + +(setq + 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\\)" + phox-comments-regexp + "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") + phox-definition-regexp (concat + "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)" + phox-comments-regexp + phox-ident-regexp) + phox-new-elim-regexp (concat + "new_elim\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" + phox-ident-regexp) + phox-new-intro-regexp (concat + "new_intro\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" + phox-ident-regexp) + phox-new-rewrite-regexp (concat + "new_rewrite\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)*[ \n\t\r)]" + phox-ident-regexp) + phox-close-def-regexp (concat + "close_def" + phox-comments-regexp + "\\(\\([^.]\\|\\(\\.[^ \n\t\r]\\)\\)+\\)[. \n\t\r]") +) + +(defun phox-find-and-forget (span) + (let (str ans tmp (lsp -1)) + (while span + (setq str (span-property span 'cmd)) + + (cond + + ((eq (span-property span 'type) 'comment)) + + ((eq (span-property span 'type) 'goalsave) + (setq ans (concat (format phox-forget-id-command + (span-property span 'name)) ans))) + + ((proof-string-match phox-new-elim-regexp str) + (setq ans + (concat (format phox-forget-new-elim-command + (match-string 3 str)) ans))) + + ((proof-string-match phox-new-intro-regexp str) + (setq ans + (concat (format phox-forget-new-intro-command + (match-string 3 str)) ans))) + + ((proof-string-match phox-new-rewrite-regexp str) + (setq ans + (concat (format phox-forget-new-rewrite-command + (match-string 3 str)) ans))) + + ((proof-string-match phox-close-def-regexp str) + (setq ans + (concat (format phox-forget-close-def-command + (match-string 4 str)) ans))) + + ((proof-string-match phox-sy-definition-regexp str) + (setq ans + (concat (format phox-forget-id-command + (concat "$" (match-string 7 str))) ans))) + + ((proof-string-match phox-definition-regexp str) + (setq ans (concat (format phox-forget-id-command + (match-string 6 str)) ans)))) + + + (setq lsp (span-start span)) + (setq span (next-span span 'type))) + + (or ans proof-no-command))) + +;;--------------------------------------------------------------------------;; +;; +;; Deleting symbols +;; +;;--------------------------------------------------------------------------;; + + +(defun phox-delete-symbol(symbol) + "Interactive function : +ask for a symbol and send a delete command to PhoX for it." + (interactive "ssymbol : ") + (proof-shell-invisible-command (concat "del " symbol ".\n"))) + +(defun phox-delete-symbol-around-point() +"Interactive function : +send a delete command to PhoX for the symbol whose name is under the cursor." + (interactive) + (let (start end) + (save-excursion + (forward-word -1) + (setq start (point)) + (forward-word 1) + (setq end (point))) + (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) + (phox-delete-symbol (buffer-substring start end)))) + +;; +;; Doing commands +;; + +(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) + (message "test") + (if (and (> (point) 1) (char-equal (char-before (point)) ?\.)) (insert "\n")) + (proof-with-script-buffer + (proof-maybe-save-point + (goto-char (proof-queue-or-locked-end)) + (proof-assert-next-command)) + (proof-maybe-follow-locked-end))) + +(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/phox-tags.el b/af2/phox-tags.el new file mode 100644 index 00000000..f2b5959a --- /dev/null +++ b/af2/phox-tags.el @@ -0,0 +1,77 @@ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; gestion des TAGS +;;--------------------------------------------------------------------------;; + +; sous xemacs, visit-tags-table n'a pas d'argument optionnel. Sous gnu emacs : + +; Normally M-x visit-tags-table sets the global value of `tags-file-name'. +; With a prefix arg, set the buffer-local value instead. + +; mieux vaut sous gnu emacs gérer la variable tags-table-list, qui +; n'existe pas sous xemacs. +; Sous xemacs il faut gérer la variable tag-table-alist qui n'existe pas +; sous gnu emacs. + +(require 'etags) + +(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 + (let ((association (cons buffer-file-name table))) + (if (member association tag-table-alist) + (message (concat table " already loaded.")) + (setq tag-table-alist (cons association tag-table-alist)))) + ; gnu emacs + (if (member table tags-table-list) + (message (concat table " already loaded.")) +; (make-local-variable 'tags-table-list) ; ne focntionne pas + (setq tags-table-list (cons table tags-table-list)) + ) + ) + ) + +(defun phox-tags-reset-table() + "Set tags-table-list to nil." + (interactive) +; (make-local-variable 'tags-table-list) + (if proof-running-on-XEmacs + (progn + (setq tag-table-alist (remassoc buffer-file-name tag-table-alist))) + (setq tags-table-list nil)) + ) + +(defun phox-tags-add-doc-table() + "Add tags in text documentation." + (interactive) + (phox-tags-add-table (concat phox-doc-dir "/text/TAGS")) + ) + +(defun phox-tags-add-lib-table() + "Add tags in libraries." + (interactive) + (phox-tags-add-table (concat phox-lib-dir "TAGS")) + ) + +(defun phox-tags-add-local-table() + "Add the tags table created with function phox-create-local-table." + (interactive) + (phox-tags-add-table (concat buffer-file-name "TAGS")) + ) + +(defun phox-tags-create-local-table() + "create table on local buffer" + (interactive) + (shell-command (concat phox-etags + " -o " + (file-name-nondirectory (buffer-file-name)) + "TAGS " + (file-name-nondirectory (buffer-file-name)))) + ) + +;; default + +(if phox-tags-doc (add-hook 'phox-mode-hook 'phox-tags-add-doc-table)) + +(provide 'phox-tags) \ No newline at end of file diff --git a/af2/phox.el b/af2/phox.el new file mode 100644 index 00000000..49f4ab15 --- /dev/null +++ b/af2/phox.el @@ -0,0 +1,229 @@ +(require 'proof) ; load generic parts + +;; Adjust toolbar entries. (Must be done +;; before proof-toolbar is loaded). + +(if proof-running-on-XEmacs (setq phox-toolbar-entries + (remassoc 'context phox-toolbar-entries))) + + +;; ======== User settings for PhoX ======== +;; +;; Defining variables using customize is pretty easy. +;; You should do it at least for your prover-specific user options. +;; +;; proof-site provides us with two customization groups +;; automatically: (based on the name of the assistant) +;; +;; '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 -> PhoX +;; The second group appears in the menu: +;; ProofGeneral -> Internals -> PhoX config +;; + +(defcustom phox-prog-name "phox -pg" + "*Name of program to run PhoX." + :type 'file + :group 'phox) + +(defcustom phox-sym-lock t + "*Whether to use sym-lock or not." + :type 'boolean + :group 'phox) + +(defcustom phox-web-page + "http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html" + "URL of web page for PhoX." + :type 'string + :group 'phox-config) + +(defcustom phox-doc-dir + "/usr/local/doc/phox" + "The name of the root documentation directory for PhoX." + :type 'string + :group 'phox-config) + +(defcustom phox-lib-dir + "/usr/local/lib/phox" + "The name of the root directory for PhoX libraries." + :type 'string + :group 'phox-config) + +(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 'phox-config) + +(defcustom phox-tags-doc + t + "*If non nil, tags table for PhoX text documentation is loaded." + :type 'boolean + :group 'phox-config) + +(defcustom phox-etags + (concat phox-doc-dir "/tools/phox_etags.sh") + "Command to build tags table." + :type 'string + :group 'phox-config) + +(require 'phox-tags) +(require 'phox-outline) +(require 'phox-font) +(require 'phox-fun) + +;; ----- PhoX specific menu + +(defpgdefault menu-entries + '( + ["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" phox-tags-create-local-table t] + ["------------------" nil nil] +; ["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] + ) + )) + +;; +;; ======== Configuration of generic modes ======== +;; + +(defun phox-config () + "Configure Proof General scripting for PhoX." + (setq + proof-terminal-char ?\. ; ends every command + proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" + 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-save-command-regexp "save" + proof-goal-with-hole-regexp (concat + "\\(prop\\|proposition\\|lem\\|lemma\\|fact\\|cor\\|corollary\\|theo\\|theorem\\)" + 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" + 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" + proof-goal-command "goal %s." + proof-save-command "save %s." + proof-kill-goal-command "abort." + proof-showproof-command "goals." + proof-undo-n-times-cmd "undo %s." + proof-find-and-forget-fn 'phox-find-and-forget + proof-find-theorems-command "search \"%s\"." + proof-auto-multiple-files nil + font-lock-keywords phox-font-lock-keywords + ) +) + +(defun phox-shell-config () + "Configure Proof General shell for PhoX." + (setq + ;proof-shell-cd-cmd "cd \"%s\"" + 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." + proof-shell-restart-cmd "quit." + proof-shell-proof-completed-regexp "^.*^proved" +)) + + +;; +;; ======== Defining the derived modes ======== +;; + +;; The name of the script mode is always -script, +;; but the others can be whatever you like. +;; +;; The derived modes set the variables, then call the +;; -config-done function to complete configuration. + +(define-derived-mode phox-mode proof-mode + "PhoX script" nil + (phox-config) + (phox-sym-lock-start) + (proof-config-done) + (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 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 phox-shell-mode proof-shell-mode + "PhoX shell" nil + (phox-shell-config) + (proof-shell-config-done)) + +(define-derived-mode phox-response-mode proof-response-mode + "PhoX response" nil + (setq + font-lock-keywords phox-font-lock-keywords + proof-output-fontify-enable t) + (phox-sym-lock-start) + (proof-response-config-done) + (font-lock-mode)) + +(define-derived-mode phox-goals-mode proof-goals-mode + "PhoX goals" nil + (setq + font-lock-keywords phox-font-lock-keywords + proof-output-fontify-enable t) + (phox-sym-lock-start) + (proof-goals-config-done) + (font-lock-mode)) + +;; The response buffer and goals buffer modes defined above are +;; trivial. In fact, we don't need to define them at all -- they +;; would simply default to "proof-response-mode" and "pbp-mode". + +;; A more sophisticated instantiation might set font-lock-keywords to +;; add highlighting, or some of the proof by pointing markup +;; configuration for the goals buffer. + +;; The final piece of magic here is a hook which configures settings +;; to get the proof shell running. Proof General needs to know the +;; name of the program to run, and the modes for the shell, response, +;; and goals buffers. + +(add-hook 'proof-pre-shell-start-hook 'phox-pre-shell-start) + +(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 '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!) -- cgit v1.2.3