From 59e99ef53e76cdb15a7609b88d996e99afe31c20 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Fri, 1 Dec 2000 17:46:38 +0000 Subject: af2 is now called PhoX --- phox/README | 19 ++++ phox/example.af2 | 9 ++ phox/phox-font.el | 138 +++++++++++++++++++++++ phox/phox-fun.el | 150 +++++++++++++++++++++++++ phox/phox-outline.el | 57 ++++++++++ phox/phox-tags.el | 77 +++++++++++++ phox/phox.el | 229 ++++++++++++++++++++++++++++++++++++++ phox/sym-lock.el | 309 +++++++++++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 988 insertions(+) create mode 100644 phox/README create mode 100644 phox/example.af2 create mode 100644 phox/phox-font.el create mode 100644 phox/phox-fun.el create mode 100644 phox/phox-outline.el create mode 100644 phox/phox-tags.el create mode 100644 phox/phox.el create mode 100644 phox/sym-lock.el (limited to 'phox') diff --git a/phox/README b/phox/README new file mode 100644 index 00000000..9c955b84 --- /dev/null +++ b/phox/README @@ -0,0 +1,19 @@ +PhoX Proof General, for Phox. + +Written by Christophe Raffalli + +$Id$ + +Status: supported +Maintainer: Christophe Raffalli +PhoX version: 0.7 +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. + + + + diff --git a/phox/example.af2 b/phox/example.af2 new file mode 100644 index 00000000..36ece411 --- /dev/null +++ b/phox/example.af2 @@ -0,0 +1,9 @@ +(* + Example proof script for AF2 Proof General + + $Id$ +*) + +prop (* test *) (* just un test *) test /\X (X -> X). +trivial. +save. \ No newline at end of file diff --git a/phox/phox-font.el b/phox/phox-font.el new file mode 100644 index 00000000..f04844fa --- /dev/null +++ b/phox/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/phox/phox-fun.el b/phox/phox-fun.el new file mode 100644 index 00000000..58771057 --- /dev/null +++ b/phox/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/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-tags.el b/phox/phox-tags.el new file mode 100644 index 00000000..f2b5959a --- /dev/null +++ b/phox/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/phox/phox.el b/phox/phox.el new file mode 100644 index 00000000..49f4ab15 --- /dev/null +++ b/phox/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/phox/sym-lock.el b/phox/sym-lock.el new file mode 100644 index 00000000..085ef268 --- /dev/null +++ b/phox/sym-lock.el @@ -0,0 +1,309 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; 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 5-96 +;; tweaked by Steve Dunham 5-96 +;; rewritten and enhanced by Albert Cohen 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 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) +(require 'atomic-extents) + +(defvar sym-lock-sym-count 0 + "Counter for internal symbols.") + +(defvar sym-lock-ext-start nil "Temporary for atomicization.") +(make-variable-buffer-local 'sym-lock-ext-start) +(defvar sym-lock-ext-end nil "Temporary for atomicization.") +(make-variable-buffer-local 'sym-lock-ext-end) + +(defvar sym-lock-font-size nil + "Default size for Sym-Lock symbol font.") +(make-variable-buffer-local 'sym-lock-font-size) +(put 'sym-lock-font-size 'permanent-local t) + +(defvar sym-lock-keywords nil + "Similar to `font-lock-keywords'.") +(make-variable-buffer-local 'sym-lock-keywords)(put 'sym-lock-keywords 'permanent-local t) + +(defvar sym-lock-enabled nil + "Sym-Lock switch.") +(make-variable-buffer-local 'sym-lock-enabled) +(put 'sym-lock-enabled 'permanent-local t) + +(defvar sym-lock-color (face-foreground 'default) + "*Sym-Lock default color in `font-lock-use-colors' mode.") +(make-variable-buffer-local 'sym-lock-color) +(put 'sym-lock-color 'permanent-local t) + +(defvar sym-lock-mouse-face 'default + "*Face for symbols when under mouse.") +(make-variable-buffer-local 'sym-lock-mouse-face) +(put 'sym-lock-mouse-face 'permanent-local t) + +(defvar sym-lock-mouse-face-enabled t + "Mouse face switch.") +(make-variable-buffer-local 'sym-lock-mouse-face-enabled) +(put 'sym-lock-mouse-face-enabled 'permanent-local t) + +(defun sym-lock-gen-symbol (&optional prefix) + "Generate a new internal symbol." + ;; where is the standard function to do this ? + (setq sym-lock-sym-count (+ sym-lock-sym-count 1)) + (intern (concat "sym-lock-gen-" (or prefix "") + (int-to-string sym-lock-sym-count)))) + +(defun sym-lock-make-symbols-atomic (&optional begin end) + "Function to make symbol faces atomic." + (if sym-lock-enabled + (map-extents + (lambda (extent maparg) + (let ((face (extent-face extent)) (ext)) + (if (and face (setq ext (face-property face 'sym-lock-remap))) + (progn + (if (numberp ext) + (set-extent-endpoints + extent (- (extent-start-position extent) ext) + (extent-end-position extent))) + (if ext + (progn + (if sym-lock-mouse-face-enabled + (set-extent-property extent 'mouse-face + 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 sym-lock-compute-font-size () + "Computes the size of the \"better\" symbol font." + (let ((num (if (fboundp 'face-height) + (face-height 'default) + (let ((str (face-font 'default))) + (if + (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*" str) + (string-to-number (substring str (match-beginning 1) + (match-end 1))))))) + (maxsize 100) (size) (oldsize) + (lf (list-fonts "-adobe-symbol-medium-r-normal--*"))) + (while (and lf maxsize) + (if + (string-match "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*" + (car lf)) + (progn + (setq size (string-to-number (substring (car lf) (match-beginning 1) + (match-end 1)))) + (if (and (> size num) (< size maxsize)) + (setq maxsize nil) + (setq oldsize size)))) + (setq lf (cdr lf))) + (number-to-string (if (and oldsize (< oldsize 100)) oldsize num)))) + +(defvar sym-lock-font-name + (if window-system + (concat "-adobe-symbol-medium-r-normal--" + (if sym-lock-font-size sym-lock-font-size + (sym-lock-compute-font-size)) + "-*-*-*-p-*-adobe-fontspecific") + "") + "Name of the font used by Sym-Lock.") +(make-variable-buffer-local 'sym-lock-font-name) +(put 'sym-lock-font-name 'permanent-local t) + +(make-face 'sym-lock-adobe-symbol-face) +(set-face-font 'sym-lock-adobe-symbol-face sym-lock-font-name) + +(defun sym-lock-set-foreground () + "Set foreground color of Sym-Lock faces." + (if (and (boundp 'sym-lock-defaults) sym-lock-defaults) + (let ((l (car sym-lock-defaults)) + (color (if (and (boundp 'font-lock-use-fonts) font-lock-use-fonts) + (face-foreground 'default) 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 sym-lock-remap-face (pat pos obj atomic) + "Make a temporary face which remaps the POS char of PAT to the +given OBJ under `sym-lock-adobe-symbol-face' and all other characters to +the empty string. OBJ may either be a string or a character." + (let* ((name (sym-lock-gen-symbol "face")) + (table (make-display-table)) + (tface (make-face name "sym-lock-remap-face" t))) + (fillarray table "") + (aset table (string-to-char (substring pat (1- pos) pos)) + (if (stringp obj) obj (make-string 1 obj))) + (set-face-foreground tface (if (and (boundp 'font-lock-use-fonts) + font-lock-use-fonts) + (face-foreground 'default) sym-lock-color)) + (set-face-property tface 'display-table table) + (set-face-property tface 'font (face-font 'sym-lock-adobe-symbol-face)) + (set-face-property tface 'sym-lock-remap atomic) ; mark it + tface ; return face value and not face name + ; the temporary face would be otherwise GCed + )) + +(defvar sym-lock-clear-face + (let* ((name (sym-lock-gen-symbol "face")) + (table (make-display-table)) + (tface (make-face name "sym-lock-remap-face" t))) + (fillarray table "") + (set-face-property tface 'display-table table) + (set-face-property tface 'sym-lock-remap 1) ; mark it + tface + ;; return face value and not face name + ;; the temporary face would be otherwise GCed + )) + +(defun 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 `sym-lock-adobe-symbol-face'. The +face's extent will become atomic." + (message "Computing Sym-Lock faces...") + (setq sym-lock-keywords (sym-lock-rec fl)) + (setq sym-lock-enabled t) + (message "Computing Sym-Lock faces... done.")) + +(defun sym-lock-rec (fl) + (let ((f (car fl))) + (if f + (cons (apply 'sym-lock-atom-face f) + (sym-lock-rec (cdr fl)))))) + +(defun 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 `sym-lock-adobe-symbol-face'. The face extent will become atomic." + (list pat num (sym-lock-remap-face pat pos obj t) override)) + +(defun sym-lock-pre-idle-hook-first () + (condition-case nil + (if (and sym-lock-enabled font-lock-old-extent) + (setq sym-lock-ext-start (extent-start-position font-lock-old-extent) + sym-lock-ext-end (extent-end-position font-lock-old-extent)) + (setq sym-lock-ext-start nil)) + (error (warn "Error caught in `sym-lock-pre-idle-hook-first'")))) + +(defun sym-lock-pre-idle-hook-last () + (condition-case nil + (if (and sym-lock-enabled sym-lock-ext-start) + (sym-lock-make-symbols-atomic sym-lock-ext-start sym-lock-ext-end)) + (error (warn "Error caught in `sym-lock-pre-idle-hook-last'")))) + +(add-hook 'font-lock-after-fontify-buffer-hook + 'sym-lock-make-symbols-atomic) + +(defun sym-lock-enable () + "Enable Sym-Lock on this buffer." + (interactive) + (if (not sym-lock-keywords) + (error "No Sym-Lock keywords defined!") + (setq 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 "Sym-Lock enabled."))) + +(defun sym-lock-disable () + "Disable Sym-Lock on this buffer." + (interactive) + (if (not sym-lock-keywords) + (error "No Sym-Lock keywords defined!") + (setq 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 "Sym-Lock disabled."))) + +(defun sym-lock-mouse-face-enable () + "Enable special face for symbols under mouse." + (interactive) + (setq sym-lock-mouse-face-enabled t) + (if sym-lock-enabled + (font-lock-fontify-buffer))) + +(defun sym-lock-mouse-face-disable () + "Disable special face for symbols under mouse." + (interactive) + (setq sym-lock-mouse-face-enabled nil) + (if sym-lock-enabled + (font-lock-fontify-buffer))) + +(defun sym-lock-font-lock-hook () + "Function called by `font-lock-mode' for initialization purposes." + (add-hook 'pre-idle-hook 'sym-lock-pre-idle-hook-first) + (add-hook 'pre-idle-hook 'sym-lock-pre-idle-hook-last t) + (add-menu-button '("Options" "Syntax Highlighting") + ["Sym-Lock" + (if sym-lock-enabled (sym-lock-disable) (sym-lock-enable)) + :style toggle :selected sym-lock-enabled + :active sym-lock-keywords] "Automatic") + (if (and (featurep 'sym-lock) sym-lock-enabled + font-lock-defaults (boundp 'sym-lock-keywords)) + (progn + (sym-lock-patch-keywords) + (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) + (sym-lock-patch-keywords)) + (turn-on-font-lock))) + +(defun sym-lock-patch-keywords () + (if (and font-lock-keywords sym-lock-enabled + (boundp '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 + "sym-lock" + (symbol-name + (face-name (cadr (cdar + font-lock-keywords)))))))) + (setq font-lock-keywords (append sym-lock-keywords + font-lock-keywords))) t) + +(add-hook 'font-lock-mode-hook 'sym-lock-font-lock-hook) + +(provide 'sym-lock) -- cgit v1.2.3