diff options
Diffstat (limited to 'phox')
| -rw-r--r-- | phox/.cvsignore | 12 | ||||
| -rw-r--r-- | phox/README | 18 | ||||
| -rw-r--r-- | phox/example.phx | 22 | ||||
| -rw-r--r-- | phox/phox-extraction.el | 170 | ||||
| -rw-r--r-- | phox/phox-font.el | 93 | ||||
| -rw-r--r-- | phox/phox-fun.el | 436 | ||||
| -rw-r--r-- | phox/phox-outline.el | 57 | ||||
| -rw-r--r-- | phox/phox-sym-lock.el | 366 | ||||
| -rw-r--r-- | phox/phox-tags.el | 115 | ||||
| -rw-r--r-- | phox/phox.el | 279 | ||||
| -rw-r--r-- | phox/x-symbol-phox.el | 202 |
11 files changed, 1770 insertions, 0 deletions
diff --git a/phox/.cvsignore b/phox/.cvsignore new file mode 100644 index 00000000..79f631e7 --- /dev/null +++ b/phox/.cvsignore @@ -0,0 +1,12 @@ +config +config.dos +*~ +#*# +*.o +*.a +*.cmo +*.cmi +*.cmx +*.pho +*.phi +*.pht diff --git a/phox/README b/phox/README new file mode 100644 index 00000000..c50f814f --- /dev/null +++ b/phox/README @@ -0,0 +1,18 @@ +PhoX Proof General, for Phox. + +Written by Christophe Raffalli + +Status: supported +Maintainer: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> +PhoX version: 0.8 +PhoX homepage: http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html + +======================================== + +This mode has support for script management with PhoX, and some +other features ported from PhoX's own Emacs mode. + +Soon compatible with x-symbol, but it does not work yet ... + +$Id$ + diff --git a/phox/example.phx b/phox/example.phx new file mode 100644 index 00000000..5dacbb20 --- /dev/null +++ b/phox/example.phx @@ -0,0 +1,22 @@ +(* + Example proof script for PhoX Proof General + + $Id$ +*) + +(* +goal /\n:N (ack n N1 >= N2). +intro 2. +elim H. +trivial. +elim -1 [case] H0. +trivial. +trivial. +save ack_lem7. +*) + +prop (* test *) (* just un test *) test /\X (X -> X). +print $0. +trivial. +save. + diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el new file mode 100644 index 00000000..b488d43e --- /dev/null +++ b/phox/phox-extraction.el @@ -0,0 +1,170 @@ +;; $State$ $Date$ $Revision$ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; program extraction. +;; +;; note : program extraction is still experimental This file is very +;; dependant of the actual state of program extraction in phox. +;;--------------------------------------------------------------------------;; +;; configuration : + +(defvar phox-prog-orig "phox -pg" "original name of phox binary.") + +(defun phox-prog-flags-modify(option) +"ask for a string that are options to pass to phox binary" +(interactive "soption :") +; pas d'analyse de la réponse, +(let ((process)) + (if (and phox-prog-name + (progn (string-match " \\|$" phox-prog-name) + (setq process + (substring phox-prog-name 0 (match-beginning 0)) + ) + ) + (processp (get-process process)) + (eq (process-status process) 'run)) + (error "Error : exit phox process first !") + ) +(if (string-match "^ *$" option) + (progn + (message + "no option other than default ones will be passed to phox binary.") + (setq phox-prog-name phox-prog-orig)) + (progn + (message (format "option %s will be passed to phox binary." option )) + (setq phox-prog-name (concat phox-prog-orig " " option)) + ) + ) +) +) + + +(defun phox-prog-flags-extract() +"pass option -f to phox binary. A program can be extracted from +proof of theorem_name with : +compile theorem_name. +output." +(interactive) +(phox-prog-flags-modify "-f") +(message +"WARNING : program extraction is experimental and can disturb the prover !") +) + +(defun phox-prog-flags-erase() +"no option to phox binary." +(interactive) +(phox-prog-flags-modify "")) + +; encore une fonction qui devrait être redéfinie en cas d'autres +; options possibles que -f + +(defun phox-toggle-extraction() +"toggle between extraction mode and ordinary mode for phox process." +(interactive) +(cond ((string-equal phox-prog-name phox-prog-orig) ;; à améliorer (espaces) + (phox-prog-flags-extract)) + ((string-match "\-f$" phox-prog-name) (phox-prog-flags-erase)) + (t (error "option must be empty or -f, use phox-prog-flags-modify."))) +) + +;; commands + +; compilation +(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))) + +(defun phox-compile-theorem-on-cursor() +"Interactive function : +send a compile command to PhoX for the theorem which name is under the cursor." + (interactive) + (let (start end) + (save-excursion +; (modify-syntax-entry ?\. "w") + (forward-word 1) + (setq start (point)) + (forward-word -1) + (setq end (point))) + (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) + (phox-compile-theorem (buffer-substring start end)))) + +; extraction + +(defun phox-output () + +"Interactive function : +send output command to phox in order to obtain programs +extracted from proofs of all compiled theorems." + + +(interactive) +(proof-shell-invisible-command "output")) + +(defun phox-output-theorem (name) +"Interactive function : +ask for the name of a theorem and send an output command to PhoX for it +in order to obtain a programm extracted from the known proof of this theorem." + (interactive "stheorem : ") + (proof-shell-invisible-command (concat "output " name))) + +(defun phox-output-theorem-on-cursor() +"Interactive function : +send an output command to PhoX for the theorem which name is under the cursor +in order to obtain a programm extracted from the known proof of this theorem." + (interactive) + (let (start + end +; (syntax (char-to-string (char-syntax ?\.))) + ) + (save-excursion +; (modify-syntax-entry ?\. "w") ; à modifier globablement ? + (forward-word 1) + (setq start (point)) + (forward-word -1) + (setq end (point))) +; (modify-syntax-entry ?\. syntax) + (if (char-equal (char-after (- end 1)) ?\.)(setq end (- end 1))) + (phox-output-theorem (buffer-substring start end)))) + +; Definitions of lambda-mu terms (tdef nom_de_term = terme.) and +; normalization (eval term.) have to be "visible" proof commands. + +;; menu + + (defvar phox-extraction-menu + '("Extraction" + ["Program extraction enabled" + phox-toggle-extraction + :style radio + :selected(string-match "\-f$" phox-prog-name) + ] + ["------------------------------" nil nil + ] + ["Compile theorem on cursor" phox-compile-theorem-on-cursor + :active(string-match "\-f$" phox-prog-name) + ] + ["Extraction for theorem on cursor" phox-output-theorem-on-cursor + :active(string-match "\-f$" phox-prog-name) + ] + ["Extraction for all compiled theorems" phox-output + :active(string-match "\-f$" phox-prog-name) + ] + ["------------------------------" nil nil + ] + ["Compile theorem : " phox-compile-theorem + :active(string-match "\-f$" phox-prog-name) + ] + ["Extraction for theorem : " phox-output-theorem + :active(string-match "\-f$" phox-prog-name) + ] + ) +"A list of menu items to deal with program extraction. +Warning, program extraction is still experimental +and can disturb the prover !" +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(provide 'phox-extraction) diff --git a/phox/phox-font.el b/phox/phox-font.el new file mode 100644 index 00000000..f58f41f3 --- /dev/null +++ b/phox/phox-font.el @@ -0,0 +1,93 @@ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; 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\\|" + "Data\\|" + "I\\(mport\\|nductive\\)\\|" + "Use\\|" + "Sort\\|" + "new_\\(intro\\|e\\(lim\\|quation\\)\\|rewrite\\)\\|" + "a\\(dd_path\\|uthor\\)\\|" + "c\\(l\\(aim\\|ose_def\\)\\|or\\(ollary\\)?\\)\\|" + "d\\(e\\(f\\(_thlist\\)?\\|l\\(_proof\\)\\)\\|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\\)?\\|ove_claim\\)\\)\\|" + "quit\\|" + "s\\(ave\\|earch\\)\\|" + "t\\(ex\\(_syntax\\)?\\|heo\\(rem\\)?\\|itle\\)" + "\\)[ \t\n\r.]") + '(0 'font-lock-keyword-face t)) +;proof command + (cons (concat "\\([ \t]\\|^\\)\\(" + "a\\(bort\\|fter\\|pply\\|xiom\\)\\|" + "by_absurd\\|" + "constraints\\|" + "elim\\|" + "from\\|" + "goals\\|" + "in\\(tros?\\|stance\\)\\|" + "l\\(oc\\(al\\|k\\)\\|efts?\\)\\|" + "next\\|" + "prove\\|" + "r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|" + "s\\(elect\\|lh\\)\\|" + "trivial\\|" + "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)" + "\\)[ \t.]") + '(0 'font-lock-type-face t)))) + +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; phox-sym-lock tables +;;--------------------------------------------------------------------------;; + +(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. +(defconst phox-sym-lock-keywords-table + '((">=" 0 1 179) + ("<=" 0 1 163) + ("!=" 0 1 185) + (":<" 0 1 206) + ("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206) + ("\\\\/" 0 1 36) + ("/\\\\" 0 1 34) + ("\\<or\\>" 0 3 218) + ("\\<in\\>" 0 3 206) + ("\\<notin\\>" 0 4 207) + ("\\<inter\\>" 0 3 199) + ("\\<union\\>" 0 3 200) + ("\\<minus\\>" 0 3 45) + ("&" 0 1 217) + ("<->" 0 1 171) + ("=>" 0 1 222) + ("\\<subset\\>" 0 4 204) + ("->" 0 1 174) + ("~" 0 1 216) + ("\\\\" 0 1 108))) +; "If non nil: Overrides default Phox-Sym-Lock patterns for PhoX.") + +(defun phox-sym-lock-start () + (if (and (featurep 'phox-sym-lock) phox-sym-lock) + (progn + (setq phox-sym-lock-color + (face-foreground 'font-lock-function-name-face)) + (if (not phox-sym-lock-keywords) + (phox-sym-lock phox-sym-lock-keywords-table))))) + +(provide 'phox-font) diff --git a/phox/phox-fun.el b/phox/phox-fun.el new file mode 100644 index 00000000..d556a3c8 --- /dev/null +++ b/phox/phox-fun.el @@ -0,0 +1,436 @@ +;; $State$ $Date$ $Revision$ +;; syntax + +(setq + phox-forget-id-command "del %s.\n" + phox-forget-proof-command "del_proof %s.\n" + phox-forget-new-elim-command "edel elim %s.\n" + phox-forget-new-intro-command "edel intro %s.\n" + phox-forget-new-equation-command "edel equation %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-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-inductive-option "\\(\\[[^]]*]\\)?" + phox-spaces-regexp "[ \n\t\r]*" + phox-sy-definition-regexp (concat + "\\(Cst\\|def\\)" + phox-comments-regexp + "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") + phox-sy-inductive-regexp (concat + "Inductive" + phox-comments-regexp + phox-inductive-option + phox-comments-regexp + "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") + phox-inductive-regexp (concat + "Inductive" + phox-comments-regexp + phox-inductive-option + phox-comments-regexp + phox-ident-regexp) + phox-data-regexp (concat + "Data" + phox-comments-regexp + phox-inductive-option + phox-comments-regexp + phox-ident-regexp) + phox-definition-regexp (concat + "\\(Cst\\|def\\(_thlist\\)?\\|claim\\|Sort\\)" + phox-comments-regexp + phox-ident-regexp) + phox-prove-claim-regexp (concat + "prove_claim" + 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-new-equation-regexp (concat + "new_equation\\([^.]\\|\\(\\.[^ \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-init-syntax-table (&optional TABLE) + "Set appropriate values for syntax table in current buffer, +or for optional argument TABLE." +;; useful for using forward-word + (modify-syntax-entry ?_ "w" TABLE) + (modify-syntax-entry ?\. "w" TABLE) +;; Configure syntax table for block comments + (modify-syntax-entry ?\* ". 23" TABLE) + (modify-syntax-entry ?\( "()1" TABLE) + (modify-syntax-entry ?\) ")(4" TABLE) +;; à compléter éventuellement +) + + +;; completions : + +(defvar phox-top-keywords +'( +"goal" +"restart" +"quit" +"theorem" +"claim" +"cst" +"Cst" +"def" +"def_thlist" +"del" +"del_proof" +"Sort" +"close_def" +"edel" +"new_elim" +"new_intro" +"new_equation" +"new_rewrite" +"Data" +"Inductive" +"add_path" +"Import" +"include" +"Use" +"tex_syntax" +"depend" +"eshow" +"flag" +"path" +"print" +"print_sort" +"priority" +"prove_claim" +"search" +"compile" +"tdef" +"eval" +"output" +"compile" +"compute" +"Local" +) +"Names of phox top commands." +) + +(defvar phox-proof-keywords +'( +"axiom" +"elim" +"intro" +"intros" +"apply" +"by_absurd" +"from" +"left" +"lefts" +"prove" +"use" +"auto" +"trivial" +"rewrite" +"rewrite_hyp" +"unfold" +"unfold_hyp" +"constraints" +"instance" +"lock" +"unlock" +"goals" +"after" +"next" +"select" +"local" +"rename" +"rmh" +"slh" +"abort" +"save" +"undo" +"Try" +) +"Name of phox proof commands." +) + + + +(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) + (if (proof-string-match phox-prove-claim-regexp str) + (setq ans (concat (format phox-forget-proof-command + (match-string 4 str)) ans)) + (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) ; deprecated + (setq ans + (concat (format phox-forget-new-equation-command + (match-string 3 str)) ans))) + + ((proof-string-match phox-new-equation-regexp str) + (setq ans + (concat (format phox-forget-new-equation-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-sy-inductive-regexp str) + (setq ans + (concat (format phox-forget-id-command + (concat "$" (match-string 10 str))) ans))) + + ((proof-string-match phox-inductive-regexp str) + (setq ans + (concat (format phox-forget-id-command + (match-string 8 str)) ans))) + + ((proof-string-match phox-data-regexp str) + (setq + name (match-string 8 str) + sname (concat (downcase (substring name 0 1)) + (substring name 1 nil)) + ans (concat (format phox-forget-id-command + sname) 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))) + +;; +;; 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) + (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))) + +;;--------------------------------------------------------------------------;; +;; Obtaining some informations on the system. +;; +;;--------------------------------------------------------------------------;; +;; All the commands in section "Obtaining some informations on the +;; system." (see cmd_top.tex) are associated to a +;; function, and appear in the submenu "State" [pr]. + +(defun phox-depend-theorem(theorem) + "Interactive function : +ask for a string and and send a depend command to PhoX for it. + +Gives the list of all axioms which have been used to prove the theorem." + +(interactive "stheorem: ") +(proof-shell-invisible-command (concat "depend " theorem))) + +(defun phox-eshow-extlist(extlist) + "Interactive function : +ask for a string and send an eshow command to PhoX for it. + +Shows the given extension-list. Possible extension lists are : equation +(the list of equations added to unification introduced by the new_equation +command), elim, intro, (the introduction and elimination rules +introduced by the new_elim and new_intro {-t} commands), closed +(closed definitions introduced by the close_def command) and tex +(introduced by the tex_syntax command)." + +(interactive "sextension list: ") +(proof-shell-invisible-command (concat "eshow " extlist))) + +(defun phox-flag-name(name) +"Interactive function : +ask for a string and send a flag command to PhoX for it. + + Print the value of an internal flag of the + system. The different flags are listed in the doc, see flag." + +(interactive "sname: ") +(proof-shell-invisible-command (concat "flag " name))) + + +(defun phox-path() +"Interactive function : + send a path command to PhoX. + + Prints the list of all paths. This path list is used to find + files when using the include command." + + +(interactive) +(proof-shell-invisible-command "path")) + +(defun phox-print-expression(expr) +"Interactive function : +ask for a string and send a print command to PhoX for it. + + In case argument expr + is a closed expression of the language in use, prints it and gives its + sort, gives an (occasionally) informative error message otherwise. In + case expr is a defined expression (constant, theorem ...) + gives the definition." + +(interactive "sexpr: ") +(proof-shell-invisible-command (concat "print " expr))) + +(defun phox-print-sort-expression(expr) +"Interactive function : +ask for a string and send a print_sort command to PhoX for it. + + Similar to print, but gives more information on sorts of bounded + variable in expressions." + +(interactive "sexpr: ") +(proof-shell-invisible-command (concat "print_sort " expr))) + + +(defun phox-priority-symbols-list(symblist) +"Interactive function : +ask for a string and send a priority command to PhoX for it. + + Print the priority of the given symbols. If no symbol are + given, print the priority of all infix and prefix symbols. +." + +(interactive "slist of symbols (possibly empty): ") +(proof-shell-invisible-command (concat "priority" symblist))) + + +(defun phox-search-string(string type) + "Interactive function: +ask for a string and possibly a type and send a search command to PhoX for it. + + Prints the list of all loaded symbols which have type and whose name + contains the string. If no type is given, it prints all symbols whose + name contains string." + +(interactive +"sstring : +stype (nothing for any type, 'a as type parameter) :") +(proof-shell-invisible-command (concat "search \"" string "\" " type))) + +;; The followings are proof commands (doc in cmd_proof.tex) : + +(defun phox-constraints() +"Interactive function : + send a constraints command to PhoX. + + Prints the constraints which should be fulfilled by unification variables, + only works in proofs." + + +(interactive) +(proof-shell-invisible-command "constraints")) + +(defun phox-goals() +"Interactive function : + send a goals command to PhoX. + + Prints the list of all remaining goals, only works in proofs." + + +(interactive) +(proof-shell-invisible-command "goals")) + +;; menu + +(defvar phox-state-menu + '("State" +["dependencies of a theorem" phox-depend-theorem t] +["show an extension list" phox-eshow-extlist t] +["value of a flag" phox-flag-name t] +["list of all paths" phox-path t] +["print expression" phox-print-expression t] +["print expression with sorts" phox-print-sort-expression t] +["priority of symbols (all if arg. empty)" phox-priority-symbols-list t] +["search for loaded symbols matching string" phox-search-string t] +["------------------" nil nil] +["constraints (proof command)" phox-constraints t] +["goals (proof command)" phox-goals t] +) +"Phox menu for informations on state of the system." +) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;--------------------------------------------------------------------------;; +;; +;; Deleting symbols +;; +;;--------------------------------------------------------------------------;; +;; obsolète probablement, sinon à modifier pour en étendre la portée. + +(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))) + +(defun phox-delete-symbol-on-cursor() +"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)))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(provide 'phox-fun) + + +
\ No newline at end of file diff --git a/phox/phox-outline.el b/phox/phox-outline.el new file mode 100644 index 00000000..766bddb3 --- /dev/null +++ b/phox/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/phox/phox-sym-lock.el b/phox/phox-sym-lock.el new file mode 100644 index 00000000..668f6e8e --- /dev/null +++ b/phox/phox-sym-lock.el @@ -0,0 +1,366 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; phox-sym-lock.el - Extension of Font-Lock mode for symbol fontification. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Copyright © 1997-1998 Albert Cohen, all rights reserved. +;; Copying is covered by the GNU General Public License. +;; +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation; either version 2 of the License, or +;; (at your option) any later version. +;; +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; History +;; +;; first prototype by wg <wg@cs.tu-berlin.de> 5-96 +;; tweaked by Steve Dunham <dunham@gdl.msu.edu> 5-96 +;; rewritten and enhanced by Albert Cohen <Albert.Cohen@prism.uvsq.fr> 3-97 +;; new symbol-face format and ergonomy improvement by Albert Cohen 2-98 +;; major step towards portability and customization by Albert Cohen 5-98 +;; removed bug with multiple appends in hook by Albert Cohen 3-99 +;; removed phox-sym-lock-face&atom which where not working by C Raffalli 4-2000 + +;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*' + +(require 'font-lock) +(proof-try-require 'atomic-extents) ;; da: proof-try-require for Emacs compat + +(defvar phox-sym-lock-sym-count 0 + "Counter for internal symbols.") + +(defvar phox-sym-lock-ext-start nil "Temporary for atomicization.") +(make-variable-buffer-local 'phox-sym-lock-ext-start) +(defvar phox-sym-lock-ext-end nil "Temporary for atomicization.") +(make-variable-buffer-local 'phox-sym-lock-ext-end) + +(defvar phox-sym-lock-font-size nil + "Default size for Phox-Sym-Lock symbol font.") +(make-variable-buffer-local 'phox-sym-lock-font-size) +(put 'phox-sym-lock-font-size 'permanent-local t) + +(defvar phox-sym-lock-keywords nil + "Similar to `font-lock-keywords'.") +(make-variable-buffer-local 'phox-sym-lock-keywords) +(put 'phox-sym-lock-keywords 'permanent-local t) + +(defvar phox-sym-lock-enabled nil + "Phox-Sym-Lock switch.") +(make-variable-buffer-local 'phox-sym-lock-enabled) +(put 'phox-sym-lock-enabled 'permanent-local t) + +(defvar phox-sym-lock-color (face-foreground 'default) + "*Phox-Sym-Lock default color in `font-lock-use-colors' mode.") +(make-variable-buffer-local 'phox-sym-lock-color) +(put 'phox-sym-lock-color 'permanent-local t) + +(defvar phox-sym-lock-mouse-face 'default + "*Face for symbols when under mouse.") +(make-variable-buffer-local 'phox-sym-lock-mouse-face) +(put 'phox-sym-lock-mouse-face 'permanent-local t) + +(defvar phox-sym-lock-mouse-face-enabled t + "Mouse face switch.") +(make-variable-buffer-local 'phox-sym-lock-mouse-face-enabled) +(put 'phox-sym-lock-mouse-face-enabled 'permanent-local t) + +(defconst phox-sym-lock-with-mule (featurep 'mule) + "Are we using Mule Xemacs ?") + +(defun phox-sym-lock-gen-symbol (&optional prefix) + "Generate a new internal symbol." + ;; where is the standard function to do this ? + (setq phox-sym-lock-sym-count (+ phox-sym-lock-sym-count 1)) + (intern (concat "phox-sym-lock-gen-" (or prefix "") + (int-to-string phox-sym-lock-sym-count)))) + + +(defun phox-sym-lock-make-symbols-atomic (&optional begin end) + "Function to make symbol faces atomic." + (if phox-sym-lock-enabled + (map-extents + (lambda (extent maparg) + (let ((face (extent-face extent)) (ext)) + (if (and face (setq ext (face-property face 'phox-sym-lock-remap))) + (progn + (if (numberp ext) + (set-extent-endpoints + extent (- (extent-start-position extent) ext) + (extent-end-position extent))) + (if ext + (progn + (if phox-sym-lock-mouse-face-enabled + (set-extent-property extent 'mouse-face + phox-sym-lock-mouse-face)) + (set-extent-property extent 'atomic t) + (set-extent-property extent 'start-open t)))))) + nil) + (current-buffer) + (if begin (save-excursion (goto-char begin) (beginning-of-line) (point)) + (point-min)) + (if end (save-excursion (goto-char end) (end-of-line) (point)) + (point-max)) + nil nil))) + +(defun phox-sym-lock-compute-font-size () + "Computes the size of the \"better\" symbol font." + (let ((font-reg (if proof-running-on-win32 + "[^:]*:[^:]*:\\([^:]*\\):[^:]*:[^:]*" + "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*")) + (font-pat (if proof-running-on-win32 + "Symbol:Regular:*::Symbol" + "-adobe-symbol-medium-r-normal--*"))) + (let ( +; face-height is not very good on win32. Why ? + (num (if (and (not proof-running-on-win32) (fboundp 'face-height)) + (face-height 'default) + (let ((str (face-font-name 'default))) + (if + (string-match font-reg str) + (string-to-number (substring str (match-beginning 1) + (match-end 1))))))) + (maxsize 100) (size) (oldsize) + (lf (list-fonts font-pat))) + (while (and lf maxsize) + (if + (string-match font-reg + (car lf)) + (let ((str-size (substring (car lf) (match-beginning 1) + (match-end 1)))) + ; test for variable size fonts. Hope it is generic ? + (if (or (equal str-size "*")(equal str-size "")) + (progn + (setq oldsize num) + (setq lf nil)) + (setq size (string-to-number str-size)) + (if (and (> size num) (< size maxsize)) + (setq lf nil) + (setq oldsize size))))) + (setq lf (cdr lf))) + (number-to-string (if (and oldsize (< oldsize maxsize)) oldsize num))))) + +(defvar phox-sym-lock-font-name + (if window-system + (if proof-running-on-win32 + (concat "Symbol:Regular:" + (if phox-sym-lock-font-size phox-sym-lock-font-size + (phox-sym-lock-compute-font-size)) + "::Symbol") + (concat "-adobe-symbol-medium-r-normal--" + (if phox-sym-lock-font-size phox-sym-lock-font-size + (phox-sym-lock-compute-font-size)) + "-*-*-*-p-*-adobe-fontspecific")) + "") + "Name of the font used by Phox-Sym-Lock.") +(make-variable-buffer-local 'phox-sym-lock-font-name) +(put 'phox-sym-lock-font-name 'permanent-local t) + +(make-face 'phox-sym-lock-adobe-symbol-face) +(if phox-sym-lock-with-mule + (progn + (make-charset 'phox-sym-lock-cset-left "Char set for symbol font" + (list 'registry "adobe-fontspecific" + 'dimension 1 + 'chars 94 + 'final 53 + 'graphic 0)) + (make-charset 'phox-sym-lock-cset-right "Char set for symbol font" + (list 'registry "adobe-fontspecific" + 'dimension 1 + 'chars 94 + 'final 54 + 'graphic 1)) + (set-face-property 'phox-sym-lock-adobe-symbol-face + 'font phox-sym-lock-font-name nil + ;; DA: removed next line, it breaks "make magic" in doc + ;; '(mule-fonts) 'prepend, + )) + (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global)) + +(defun phox-sym-lock-set-foreground () + "Set foreground color of Phox-Sym-Lock faces." + (if (and (boundp 'phox-sym-lock-defaults) phox-sym-lock-defaults) + (let ((l (car phox-sym-lock-defaults)) + (color (if (and (boundp 'font-lock-use-fonts) font-lock-use-fonts) + (face-foreground 'default) phox-sym-lock-color))) + (if (and (consp l) (eq (car l) 'quote)) (setq l (eval l))) + (if (symbolp l) (setq l (eval l))) + (dolist (c l) + (setq c (nth 2 c)) + (if (consp c) (setq c (eval c))) + (if (string-match "-adobe-symbol-" (font-name (face-font c))) + (set-face-foreground c color)))))) + +(defun phox-sym-lock-translate-char (char) + (if phox-sym-lock-with-mule + (let ((code (if (integerp char) char (char-int char)))) + (if (< code 128) + (make-char 'phox-sym-lock-cset-left obj) + (make-char 'phox-sym-lock-cset-right (- obj 128)))) + char)) + +(defun phox-sym-lock-translate-char-or-string (obj) + (if (stringp obj) + (if phox-sym-lock-with-mule + (concat (mapcar phox-sym-lock-translate-char obj)) + (obj)) + (make-string 1 (phox-sym-lock-translate-char obj)))) + +(defun phox-sym-lock-remap-face (pat pos obj atomic) + "Make a temporary face which remaps the POS char of PAT to the +given OBJ under `phox-sym-lock-adobe-symbol-face' and all other characters to +the empty string. OBJ may either be a string or a character." + (let* ((name (phox-sym-lock-gen-symbol "face")) + (table (make-display-table)) + (tface (make-face name "phox-sym-lock-remap-face" t))) + (fillarray table "") + (aset table (string-to-char (substring pat (1- pos) pos)) + (phox-sym-lock-translate-char-or-string obj)) + (set-face-foreground tface (if (and (boundp 'font-lock-use-fonts) + font-lock-use-fonts) + (face-foreground 'default) phox-sym-lock-color)) + (set-face-property tface 'display-table table) + (set-face-property tface 'font (face-font 'phox-sym-lock-adobe-symbol-face)) + (set-face-property tface 'phox-sym-lock-remap atomic) ; mark it + tface ; return face value and not face name + ; the temporary face would be otherwise GCed + )) + +(defvar phox-sym-lock-clear-face + (let* ((name (phox-sym-lock-gen-symbol "face")) + (table (make-display-table)) + (tface (make-face name "phox-sym-lock-remap-face" t))) + (fillarray table "") + (set-face-property tface 'display-table table) + (set-face-property tface 'phox-sym-lock-remap 1) ; mark it + tface + ;; return face value and not face name + ;; the temporary face would be otherwise GCed + )) + +(defun phox-sym-lock (fl) + "Create font-lock table entries from a list of (PAT NUM POS OBJ) where +PAT (at NUM) is substituted by OBJ under `phox-sym-lock-adobe-symbol-face'. The +face's extent will become atomic." + (message "Computing Phox-Sym-Lock faces...") + (setq phox-sym-lock-keywords (phox-sym-lock-rec fl)) + (setq phox-sym-lock-enabled t) + (message "Computing Phox-Sym-Lock faces... done.")) + +(defun phox-sym-lock-rec (fl) + (let ((f (car fl))) + (if f + (cons (apply 'phox-sym-lock-atom-face f) + (phox-sym-lock-rec (cdr fl)))))) + +(defun phox-sym-lock-atom-face (pat num pos obj &optional override) + "Define an entry for the font-lock table which substitutes PAT (at NUM) by +OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic." + (list pat num (phox-sym-lock-remap-face pat pos obj t) override)) + +(defun phox-sym-lock-pre-idle-hook-first () + (condition-case nil + (if (and phox-sym-lock-enabled font-lock-old-extent) + (setq phox-sym-lock-ext-start (extent-start-position font-lock-old-extent) + phox-sym-lock-ext-end (extent-end-position font-lock-old-extent)) + (setq phox-sym-lock-ext-start nil)) + (error (setq phox-sym-lock-ext-start nil)))) + +(defun phox-sym-lock-pre-idle-hook-last () + (condition-case nil + (if (and phox-sym-lock-enabled phox-sym-lock-ext-start) + (phox-sym-lock-make-symbols-atomic phox-sym-lock-ext-start phox-sym-lock-ext-end)) + (error (warn "Error caught in `phox-sym-lock-pre-idle-hook-last'")))) + +(add-hook 'font-lock-after-fontify-buffer-hook + 'phox-sym-lock-make-symbols-atomic) + +(defun phox-sym-lock-enable () + "Enable Phox-Sym-Lock on this buffer." + (interactive) + (if (not phox-sym-lock-keywords) + (error "No Phox-Sym-Lock keywords defined!") + (setq phox-sym-lock-enabled t) + (if font-lock-mode + (progn +; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! + (font-lock-set-defaults t) + (font-lock-fontify-buffer))) + (message "Phox-Sym-Lock enabled."))) + +(defun phox-sym-lock-disable () + "Disable Phox-Sym-Lock on this buffer." + (interactive) + (if (not phox-sym-lock-keywords) + (error "No Phox-Sym-Lock keywords defined!") + (setq phox-sym-lock-enabled nil) + (if font-lock-mode + (progn +; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! + (font-lock-set-defaults t) + (font-lock-fontify-buffer))) + (message "Phox-Sym-Lock disabled."))) + +(defun phox-sym-lock-mouse-face-enable () + "Enable special face for symbols under mouse." + (interactive) + (setq phox-sym-lock-mouse-face-enabled t) + (if phox-sym-lock-enabled + (font-lock-fontify-buffer))) + +(defun phox-sym-lock-mouse-face-disable () + "Disable special face for symbols under mouse." + (interactive) + (setq phox-sym-lock-mouse-face-enabled nil) + (if phox-sym-lock-enabled + (font-lock-fontify-buffer))) + +(defun phox-sym-lock-font-lock-hook () + "Function called by `font-lock-mode' for initialization purposes." + (add-hook 'pre-idle-hook 'phox-sym-lock-pre-idle-hook-first) + (add-hook 'pre-idle-hook 'phox-sym-lock-pre-idle-hook-last t) + (add-menu-button '("Options" "Syntax Highlighting") + ["Phox-Sym-Lock" + (if phox-sym-lock-enabled (phox-sym-lock-disable) (phox-sym-lock-enable)) + :style toggle :selected phox-sym-lock-enabled + :active phox-sym-lock-keywords] "Automatic") + (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled + font-lock-defaults (boundp 'phox-sym-lock-keywords)) + (progn + (phox-sym-lock-patch-keywords) + (phox-sym-lock-set-foreground)))) + +(defun font-lock-set-defaults (&optional explicit-defaults) + (when + (and + (featurep 'font-lock) + (if font-lock-auto-fontify + (not (memq major-mode font-lock-mode-disable-list)) + (memq major-mode font-lock-mode-enable-list)) + (font-lock-set-defaults-1 explicit-defaults) + (phox-sym-lock-patch-keywords)) + (turn-on-font-lock))) + +(defun phox-sym-lock-patch-keywords () + (if (and font-lock-keywords phox-sym-lock-enabled + (boundp 'phox-sym-lock-keywords) + (listp (car font-lock-keywords)) + (listp (cdar font-lock-keywords)) + (listp (cddar font-lock-keywords)) + (or (listp (caddar font-lock-keywords)) + (not (string-match + "phox-sym-lock" + (symbol-name + (face-name (cadr (cdar + font-lock-keywords)))))))) + (setq font-lock-keywords (append phox-sym-lock-keywords + font-lock-keywords))) t) + +(add-hook 'font-lock-mode-hook 'phox-sym-lock-font-lock-hook) + +(provide 'phox-sym-lock) diff --git a/phox/phox-tags.el b/phox/phox-tags.el new file mode 100644 index 00000000..e24e6ce7 --- /dev/null +++ b/phox/phox-tags.el @@ -0,0 +1,115 @@ +;; $State$ $Date$ $Revision$ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; 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 "%s already loaded." table) + (setq tag-table-alist (cons association tag-table-alist)))) + ; gnu emacs + (if (member table tags-table-list) + (message "%s already loaded." table) +; (make-local-variable 'tags-table-list) ; ne fonctionne 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)))) + ) + + +(defun phox-complete-tag() +"Complete symbol using tags table. Works with FSF emacs. + Problems with xemacs." +;; xemacs build a table for completion, tag-completion-table this table +;; donnot contains key words that use ".". There is a problem with +;; syntax-table. In xemacs you need to redefine +;; add-to-tag-completion-table, in order to add your file-type and +;; syntax-table. The modification is very simple, there should be an +;; hook for that. +;; +(interactive) +(if proof-running-on-XEmacs + (tag-complete-symbol) + (complete-tag) + ) +) + +;; menu + +(defvar phox-tags-menu + '("Tags" + ["create a tags table for local buffer" phox-tags-create-local-table t] + ["------------------" nil nil] + ["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 ..." phox-complete-tag t] + ) +"Phox menu for dealing with tags" +) + +(provide 'phox-tags) + + + diff --git a/phox/phox.el b/phox/phox.el new file mode 100644 index 00000000..88d4588a --- /dev/null +++ b/phox/phox.el @@ -0,0 +1,279 @@ +;; $State$ $Date$ $Revision$ + +(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-fun) +(require 'phox-font) +(require 'phox-extraction) +(require 'phox-tags) +(require 'phox-outline) + +;; default for tags [da: moved here to fix compilation 15/02/03] + +(if phox-tags-doc + (add-hook 'phox-mode-hook 'phox-tags-add-doc-table)) + + +;; ----- PhoX specific menu + +(defpgdefault menu-entries + (cons + phox-state-menu + (cons + phox-tags-menu + (cons + phox-extraction-menu +;; not useful ? +; '(["Delete symbol around cursor" phox-delete-symbol-around-point t] +; ["Delete symbol" phox-delete-symbol t]) + nil))) + ) + +;; +;; ======== 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-script-comment-start "(*" + proof-script-comment-end "*)" + proof-state-command "goals." + proof-goal-command-regexp + "\\`\\(Local[ \t\n\r]+\\)?\\(goal[ \t\n\r]\\|pro\\(p\\(osition\\)?\\|ve_claim\\)\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" + proof-save-command-regexp "\\`save" + proof-goal-with-hole-regexp + (concat + "\\`\\(Local[ \t\n\r]+\\)?\\(pro\\(p\\(osition\\)?\\|ve_claim\\)\\(osition\\)?\\|lem\\(ma\\)?\\|fact\\|cor\\(ollary\\)?\\|theo\\(rem\\)?\\)" + phox-strict-comments-regexp + phox-ident-regexp) + proof-goal-with-hole-result 16 + proof-save-with-hole-regexp + (concat + "\\`save" + phox-strict-comments-regexp + phox-ident-regexp) + proof-save-with-hole-result 8 + proof-ignore-for-undo-count "\\`\\(constraints\\|flag\\|goals\\|pri\\(nt\\(_sort\\)?\\|ority\\)\\|eshow\\|search\\|depend\\)" + proof-non-undoables-regexp "\\`\\(undo\\|abort\\)" + proof-shell-error-regexp "^\\([^ \n\t\r]* \\)?\\(\\(e\\|E\\)rror\\)\\|\\(\\(f\\|F\\)ailure\\)" + 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 (append phox-font-lock-keywords proof-xsym-font-lock-keywords) + ) + (phox-init-syntax-table) +;; the following is only useful for xemacs + (define-key phox-mode-map [(meta ?.)] 'phox-complete-tag) +) + +(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 "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]* goals? created\\)" + proof-shell-end-goals-regexp "^End of goals." + proof-shell-quit-cmd "quit." + proof-shell-restart-cmd "restart." + proof-shell-proof-completed-regexp "^.*^proved" + ;; pg-subterm-first-special-char ?\371 + ;; proof-shell-wakeup-char ?\371 + ;; pg-subterm-start-char ?\371 + ;; pg-subterm-sep-char ?\372 + ;; pg-topterm-char ?\373 + ;; pg-subterm-end-char ?\374 + ;; proof-shell-eager-annotation-start "\376" + ;; proof-shell-eager-annotation-start-length 1 + ;; proof-shell-eager-annotation-end "\377" +; proof-shell-annotated-prompt-regexp "Lego> \371" +; proof-shell-result-start "\372 Pbp result \373" +; proof-shell-result-end "\372 End Pbp result \373" +; proof-shell-start-goals-regexp "\372 Start of Goals \373" +; proof-shell-end-goals-regexp "\372 End of Goals \373" +; proof-shell-pre-sync-init-cmd "Configure AnnotateOn;" +)) + + +;; +;; ======== Defining the derived modes ======== +;; + +;; The name of the script mode is always <proofsym>-script, +;; but the others can be whatever you like. +;; +;; The derived modes set the variables, then call the +;; <mode>-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-on-cursor) +) + +(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 (append phox-font-lock-keywords proof-xsym-font-lock-keywords) + proof-output-fontify-enable t) + (phox-sym-lock-start) + (if (and (featurep 'phox-sym-lock) phox-sym-lock) + (add-hook 'proof-shell-handle-delayed-output-hook + 'phox-sym-lock-font-lock-hook) + ) + (proof-response-config-done)) + +(define-derived-mode phox-goals-mode proof-goals-mode + "PhoX goals" nil + (setq + font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) + proof-output-fontify-enable t) + (phox-sym-lock-start) + (if (and (featurep 'phox-sym-lock) phox-sym-lock) + (add-hook 'pg-before-fontify-output-hook + 'phox-sym-lock-font-lock-hook)) + (proof-goals-config-done)) + +;; The response buffer and goals buffer modes defined above are +;; trivial. In fact, we don't need t²o define them at all -- they +;; would simply default to "proof-response-mode" and "pg-goals-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)) + +; completions +; dans completions.el +;(setq completion-min-length 6) +;(setq completion-prefix-min-length 3) les mots de moins de 6 caractères +; ne sont pas pris en compte. Les prefixes de moins de 3 caractères ne +; sont pas non plus pris en compte. + +; (set-variable 'phox-completion-table +(defpgdefault completion-table + (append phox-top-keywords phox-proof-keywords) +) + +(eval-after-load "x-symbol-phox" + ;; Add x-symbol tokens to phox-completion-table and rebuild + ;; internal completion table if completion is already active +'(progn + (defpgdefault completion-table + (append (proof-ass completion-table) + (mapcar (lambda (xsym) (nth 2 xsym)) + x-symbol-phox-table))) + (setq proof-xsym-font-lock-keywords + x-symbol-phox-font-lock-keywords) + (if (featurep 'completion) + (proof-add-completions)))) + +(provide 'phox) + + diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el new file mode 100644 index 00000000..122ccf93 --- /dev/null +++ b/phox/x-symbol-phox.el @@ -0,0 +1,202 @@ +;; x-symbol-phox.el +;; Token language "PhoX Symbols" for package x-symbol +;; +;; ID: $Id$ +;; Author: C. Raffalli +;; Updates by Markus Wenzel, Christoph Wedler, David Aspinall. +;; Copyright 1998 Technische Universitaet Muenchen +;; License GPL (GNU GENERAL PUBLIC LICENSE) +;; +;; Adapted from x-symbol-isabelle.el +;; NB: Part of Proof General distribution. +;; + +;; CW: this sexpr can be deleted with X-Symbol 4.4.3 +(eval-when-compile + ;; Next lines should allow this file to work standalone + ;; without proof-x-symbol.el. See comments further below too. + (require 'cl) + (ignore-errors (require 'x-symbol-vars))) + +(defvar x-symbol-phox-required-fonts nil) + +;;;=========================================================================== +;;; General language accesses, see `x-symbol-language-access-alist' +;;;=========================================================================== + +;; NB da: these next two are also set in proof-x-symbol.el, but +;; it would be handy to be able to use this file away from PG. +;; FIXME: In future could fix things so just +;; (require 'proof-x-symbol) would be enough here. +(defvar x-symbol-phox-name "PhoX Symbol") +(defvar x-symbol-phox-modeline-name "phox") + +(defcustom x-symbol-phox-header-groups-alist nil + "*If non-nil, used in isasym specific grid/menu. +See `x-symbol-header-groups-alist'." + :group 'x-symbol-phox + :group 'x-symbol-input-init + :type 'x-symbol-headers) + +(defcustom x-symbol-phox-electric-ignore nil +;; "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~=" + "*Additional Phox version of `x-symbol-electric-ignore'." + :group 'x-symbol-phox + :group 'x-symbol-input-control + :type 'x-symbol-function-or-regexp) + +(defvar x-symbol-phox-required-fonts nil + "List of features providing fonts for language `phox'.") + +(defvar x-symbol-phox-extra-menu-items nil + "Extra menu entries for language `phox'.") + + +(defvar x-symbol-phox-token-grammar + ;; CW: for X-Symbol-4.4.3: + ;; '(x-symbol-make-grammar ...) + (if (fboundp 'x-symbol-make-grammar) ;; x-symbol >=4.3 versions + (x-symbol-make-grammar + :encode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . + ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) + :decode-spec nil + :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" + :token-list #'x-symbol-phox-default-token-list))) + +(defvar x-symbol-phox-input-token-grammar + '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" + ((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) + (id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]")) + "Grammar of input method Token for language `phox'.") + +(defun x-symbol-phox-default-token-list (tokens) + (mapcar + (lambda (x) + (cons x + (cond + ;; CW: where are the shapes `id' and `op' used? + ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x) + 'id) + ((string-match "\\`[<>!+-*/|&]+\\'" x) + 'op)))) + tokens)) + +(defvar x-symbol-phox-user-table nil + "User table defining Phox commands, used in `x-symbol-phox-table'.") + +(defvar x-symbol-phox-generated-data nil + "Internal.") + + +;;;=========================================================================== +;;; No image support +;;;=========================================================================== + +(defvar x-symbol-phox-master-directory 'ignore) +(defvar x-symbol-phox-image-searchpath '("./")) +(defvar x-symbol-phox-image-cached-dirs '("images/" "pictures/")) +(defvar x-symbol-phox-image-file-truename-alist nil) +(defvar x-symbol-phox-image-keywords nil) + +;;;=========================================================================== +;;; Charsym Info +;;;=========================================================================== + +(defcustom x-symbol-phox-class-alist + '((VALID "Phox Symbol" (x-symbol-info-face)) + (INVALID "no Phox Symbol" (red x-symbol-info-face))) + "Alist for Phox's token classes displayed by info in echo area. +See `x-symbol-language-access-alist' for details." + :group 'x-symbol-texi + :group 'x-symbol-info-strings + :set 'x-symbol-set-cache-variable + :type 'x-symbol-class-info) + + +(defcustom x-symbol-phox-class-face-alist nil + "Alist for Phox's color scheme in TeXinfo's grid and info. +See `x-symbol-language-access-alist' for details." + :group 'x-symbol-phox + :group 'x-symbol-input-init + :group 'x-symbol-info-general + :set 'x-symbol-set-cache-variable + :type 'x-symbol-class-faces) + + +(defvar x-symbol-phox-font-lock-keywords x-symbol-nomule-font-lock-keywords) +(defvar x-symbol-phox-font-lock-allowed-faces t) + +;;;=========================================================================== +;;; The tables +;;;=========================================================================== + +(defvar x-symbol-phox-case-insensitive nil) +(defvar x-symbol-phox-token-shape nil) +(defvar x-symbol-phox-input-token-ignore nil) + +;; FIXME: next one not needed in X-Symbol 4, kept for back compat. +;;(defvar x-symbol-phox-exec-specs +;; '(nil ("\\`\\\\<[A-Za-z][A-Za-z0-9_']*>\\'" . +;; "\\\\<[A-Za-z][A-Za-z0-9_']*>"))) + +(defvar x-symbol-phox-token-list 'identity) + +(defvar x-symbol-phox-xsymb0-table ; symbols + '((greaterequal ">=") + (lessequal "<=") + (notequal "!=") + (element "in") + (notelement "notin") + (propersubset "<<") + (intersection "inter") + (union "union") + (backslash3 "minus") + (universal1 "/\\") + (existential1 "\\/") + (logicalor "or") + (logicaland "&") + (arrowboth "<->") + (arrowright "->") + (arrowdblright "=>") + (notsign "~") + (lambda "\\") +)) + +(defun x-symbol-phox-prepare-table (table) + "Prepar the table." + (mapcar (lambda (entry) + (list (car entry) nil + (cadr entry))) + table)) + +(defvar x-symbol-phox-table + (x-symbol-phox-prepare-table + (append x-symbol-phox-user-table x-symbol-phox-xsymb0-table))) + +(provide 'x-symbol-phox) + +;;;=========================================================================== +;;; Internal +;;;=========================================================================== +;; CW: all are not needed in X-Symbol >= v4.3 + +(defvar x-symbol-phox-menu-alist nil + "Internal. Alist used for Isasym specific menu.") +(defvar x-symbol-phox-grid-alist nil + "Internal. Alist used for Isasym specific grid.") + +(defvar x-symbol-phox-decode-atree nil + "Internal. Atree used by `x-symbol-token-input'.") +(defvar x-symbol-phox-decode-alist nil + "Internal. Alist used for decoding of Isasym macros.") +(defvar x-symbol-phox-encode-alist nil + "Internal. Alist used for encoding to Isasym macros.") + +;; FIXME: next two not needed for newer X-Symbol versions. +(defvar x-symbol-phox-nomule-decode-exec nil + "Internal. File name of Isasym decode executable.") +(defvar x-symbol-phox-nomule-encode-exec nil + "Internal. File name of Isasym encode executable.") + +(provide 'x-symbol-phox) + |