diff options
| -rw-r--r-- | lego.el | 245 | ||||
| -rw-r--r-- | proof.el | 59 |
2 files changed, 148 insertions, 156 deletions
@@ -260,7 +260,7 @@ (append lego-font-lock-keywords-1 (list (cons (ids-to-regexp lego-shell-keywords) - 'font-lock-keywords-name-face) + 'font-lock-keyword-face) '("\\<defn\\> \\([^ \t\n\)]+\\) =" 1 font-lock-function-name-face) '("^\\(value of\\|type of\\) \\([^ \t\n\)]+\\) =" 2 font-lock-function-name-face) @@ -323,23 +323,6 @@ (setq path-name "."))) (string-to-list path-name lego-path-separator))) -(defun lego-add-common-bindings (map) - "*adds keybindings used in both lego-mode and lego-shell." - (define-key map "\M-\C-i" - (if (fboundp 'complete-tag) - 'complete-tag ; Emacs 19.31 (superior etags) - 'tag-complete-symbol)) ;XEmacs 19.13 (inferior etags) - (define-key map "\C-c\C-s" 'legogrep) - (define-key map "\C-c\C-p" 'lego-prf) - (define-key map "\C-ci" 'lego-intros) - (define-key map "\C-cI" 'lego-Intros) - (define-key map "\C-cr" 'lego-Refine) - (define-key map "\C-c\C-k" 'lego-killref) - (define-key map "\C-c\C-u" 'lego-undo-1) - (define-key map "\C-c\C-t" 'lego-restart-goal) - (define-key map "\C-c\C-c" 'proof-interrupt-subjob) - map) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Commands specific to lego ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -395,7 +378,7 @@ (proof-start-shell)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Line width auto-adjust ;; +;; Lego shell startup and exit hooks ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defvar lego-shell-current-line-width nil @@ -422,28 +405,36 @@ (defun lego-shell-zap-line-width () (setq lego-shell-current-line-width nil)) - -(defun lego-shell-init-lego () - (setq compilation-search-path (cons nil (lego-get-path))) + +(defun lego-shell-start-pp () (cond (lego-pretty-p (setq lego-shell-current-line-width nil) (accept-process-output (get-process proof-shell-process-name)) (proof-simple-send lego-pretty-on t)))) +(defun lego-shell-pre-shell-start () + (setq proof-shell-prog-name lego-shell-prog-name) + (setq proof-shell-process-name lego-shell-process-name) + (setq proof-shell-buffer-name (concat "*" lego-shell-process-name "*")) + (setq proof-shell-prompt-pattern lego-shell-prompt-pattern)) + (setq proof-shell-mode-is 'lego-shell-mode) +;; (Note that emacs can't cope with aliases to buffer local variables) + +(defun lego-shell-post-shell-start () + (lego-shell-start-pp) + (setq compilation-search-path (cons nil (lego-get-path))) + (add-hook 'proof-safe-send-hook 'lego-adjust-line-width) + (add-hook 'proof-shell-exit-hook 'lego-zap-line-width) + (font-lock-fontify-buffer)) + + +(add-hook 'proof-pre-shell-start-hook 'lego-shell-pre-shell-start) +(add-hook 'proof-post-shell-start-hook 'lego-shell-post-shell-start) ;;;;;;;;;;;;;;;;;;;;;;; ;; Make support ;; ;;;;;;;;;;;;;;;;;;;;;;; -(defun possibly-save-current-buffer () - "If the buffer has been modified, the user will be asked if it -should be saved and appropriate action will be taken. This code was -nicked from AUCTeX's tex-buffer.el" - (and (buffer-modified-p) - (or (not lego-save-query) - (y-or-n-p (concat "Save file " - (buffer-file-name) - "? "))) - (save-buffer))) +(defvar lego-tmp-dir nil) (defun lego-module-name (file) "Extract the name of the module from a file." @@ -452,102 +443,65 @@ nicked from AUCTeX's tex-buffer.el" (defun lego-make-buffer () "Save file then execute a Make command on it." (interactive) - (possibly-save-current-buffer) + (and (buffer-modified-p) + (or (not lego-save-query) + (y-or-n-p (concat "Save file " + (buffer-file-name) + "? "))) + (save-buffer)) (let ((module-name (lego-module-name buffer-file-name))) (proof-simple-send (concat lego-make-command " " module-name ";") t))) (defun lego-make-buffer-until-point () - "Comment out anything after point, then save file and run a Make" + "Save from start of buffer until point, then run a Make" (interactive) - (let ((current-buffer (current-buffer)) - (temp-buffer (generate-new-buffer "*LEGO TMP*"))) - (save-excursion - (set-buffer temp-buffer) - (insert-buffer current-buffer)) - (let ((current-point (point))) - (insert proof-comment-start) - (goto-char (point-max)) - (insert proof-comment-end) - (lego-make-buffer) - (erase-buffer) - (insert-buffer temp-buffer) - (goto-char current-point)) - (kill-buffer temp-buffer))) + (let ((file (concat lego-tmp-dir "/" + (lego-module-name buffer-file-name) ".l"))) + (write-region (point-min) (point) file) + (proof-simple-send + (concat lego-make-command " \"" file "\";") t))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuring proof mode and setting up various utilities ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun lego-shell-mode-config () - - (lego-add-common-bindings lego-shell-mode-map) - (easy-menu-add lego-shell-menu lego-shell-mode-map) - (define-key lego-shell-mode-map - (if running-xemacs [(meta button1)] [S-down-mouse-1]) - 'lego-x-mouse-refine-point)) - - ;; in XEmacs 19.11 [S-down-mouse-1] is bound to - ;; `mouse-track-adjust' - ;; in Emacs 19.28 [(meta button1)] is bound to - ;; `mouse-drag-secondary' +(defun lego-common-config () - -(defun lego-mode-config () - -;; ----- things before proof-mode-child-config-done are mandatory. +;; The following things *must* be set before proof-config-done (setq proof-terminal-char ?\;) (setq proof-comment-start "(*") (setq proof-comment-end "*)") - (modify-syntax-entry ?_ "w" lego-mode-syntax-table) - (modify-syntax-entry ?\* ". 23" lego-mode-syntax-table) - (modify-syntax-entry ?\( "()1" lego-mode-syntax-table) - (modify-syntax-entry ?\) ")(4" lego-mode-syntax-table) -;; These should really be defvaralias, since if the user changes them -;; interactively proof mode won't see the alterations. Unfortunately -;; emacs can't cope with aliases to buffer local variables - - (setq proof-shell-prog-name lego-shell-prog-name) - (setq proof-shell-process-name lego-shell-process-name) - (setq proof-shell-prompt-pattern lego-shell-prompt-pattern) - (setq proof-shell-working-dir lego-shell-working-dir) - (setq proof-shell-mode-is 'lego-shell-mode) - - (proof-mode-child-config-done) - -;; ---------- Everything below here is strictly optional - it's mostly -;; ---------- just support for minor modes - - -;; where to find files - - (setq compilation-search-path (cons nil (lego-get-path))) - -;; hooks to support automatic line-width adjustment - - (add-hook 'proof-shell-safe-send-hook 'lego-adjust-line-width) - (add-hook 'proof-shell-exit-hook 'lego-shell-zap-line-width) - (add-hook 'proof-shell-pre-display-hook 'lego-shell-init-lego) - -;; keymaps and menus + (modify-syntax-entry ?_ "w") + (modify-syntax-entry ?\* ". 23") + (modify-syntax-entry ?\( "()1") + (modify-syntax-entry ?\) ")(4") - (lego-add-common-bindings lego-mode-map) + (proof-config-done) - ;; tms - I don't understand why "(control c) ?;" works, yet - ;; "(control c) proof-terminal-char" doesn't - (define-key lego-mode-map [(control c) ?;] - 'proof-active-terminator-minor-mode) - (define-key lego-mode-map proof-terminal-char 'proof-active-terminator) - - (define-key lego-mode-map [(control c) (control b)] 'lego-make-buffer) - (define-key lego-mode-map [(control c) (control h)] - 'lego-make-buffer-until-point) + (define-key (current-local-map) "\M-\C-i" + (if (fboundp 'complete-tag) + 'complete-tag ; Emacs 19.31 (superior etags) + 'tag-complete-symbol)) ;XEmacs 19.13 (inferior etags) + (define-key (current-local-map) "\C-c\C-s" 'legogrep) + (define-key (current-local-map) "\C-c\C-p" 'lego-prf) + (define-key (current-local-map) "\C-ci" 'lego-intros) + (define-key (current-local-map) "\C-cI" 'lego-Intros) + (define-key (current-local-map) "\C-cr" 'lego-Refine) + (define-key (current-local-map) "\C-c\C-k" 'lego-killref) + (define-key (current-local-map) "\C-c\C-u" 'lego-undo-1) + (define-key (current-local-map) "\C-c\C-t" 'lego-restart-goal) - (easy-menu-add lego-mode-menu lego-mode-map) +;; outline + + (make-local-variable 'outline-regexp) + (setq outline-regexp lego-outline-regexp) -;; etags support for Emacs 19.31 + (make-local-variable 'outline-heading-end-regexp) + (setq outline-heading-end-regexp lego-outline-heading-end-regexp) +;; tags (cond ((boundp 'tags-table-list) (make-local-variable 'tags-table-list) (setq tags-table-list (cons lego-tags tags-table-list)) @@ -556,39 +510,43 @@ nicked from AUCTeX's tex-buffer.el" ("lego" . lego-tags)) tag-table-alist)))) -;; outline - - (make-local-variable 'outline-regexp) - (setq outline-regexp lego-outline-regexp) +;; font lock hacks - (make-local-variable 'outline-heading-end-regexp) - (setq outline-heading-end-regexp lego-outline-heading-end-regexp) + (font-lock-mode) + (remove-hook 'font-lock-after-fontify-buffer-hook 'lego-zap-commas-buffer t) + (add-hook 'font-lock-after-fontify-buffer-hook 'lego-zap-commas-buffer nil t) + + (remove-hook 'font-lock-mode-hook 'lego-fixup-change t) + (add-hook 'font-lock-mode-hook 'lego-fixup-change nil t) + + ;; if we don't have the following, zap-commas fails to work. -;; hooks for font locks + (setq font-lock-always-fontify-immediately t) -(cond (running-xemacs - (put 'lego-mode 'font-lock-keywords 'lego-font-lock-keywords-1) - (put 'lego-shell 'font-lock-keywords - 'lego-shell-font-lock-keywords-1)) +) + + +(defun lego-mode-config () - (running-emacs19 - (add-hook 'lego-mode-hook - '(lambda () (setq font-lock-keywords - lego-font-lock-keywords-1))) - - (add-hook 'lego-shell-post-display-hook - '(lambda () (setq font-lock-keywords - lego-shell-font-lock-keywords-1))))) + (lego-common-config) + +;; where to find files -(remove-hook 'font-lock-after-fontify-buffer-hook 'lego-zap-commas-buffer t) -(add-hook 'font-lock-after-fontify-buffer-hook 'lego-zap-commas-buffer nil t) + (setq compilation-search-path (cons nil (lego-get-path))) + (or lego-tmp-dir + (make-directory + (setq lego-tmp-dir (make-temp-name "/tmp/lego")))) -(remove-hook 'font-lock-mode-hook 'lego-fixup-change t) -(add-hook 'font-lock-mode-hook 'lego-fixup-change nil t) +;; keymaps and menus + (define-key lego-mode-map [(control c) (control b)] 'lego-make-buffer) + (define-key lego-mode-map [(control c) (control h)] + 'lego-make-buffer-until-point) -;; if we don't have the following, zap-commas fails to work. + (easy-menu-add lego-mode-menu lego-mode-map) -(setq font-lock-always-fontify-immediately t) +;; font-lock + (setq font-lock-keywords lego-font-lock-keywords-1) + (font-lock-fontify-buffer) ;; insert standard header and footer in fresh buffers @@ -601,4 +559,27 @@ nicked from AUCTeX's tex-buffer.el" ))) ) + + +(defun lego-shell-mode-config () + + (lego-common-config) + + (define-key lego-shell-mode-map + (if running-xemacs [(meta button1)] [S-down-mouse-1]) + 'lego-x-mouse-refine-point) + + ;; in XEmacs 19.11 [S-down-mouse-1] is bound to + ;; `mouse-track-adjust' + ;; in Emacs 19.28 [(meta button1)] is bound to + ;; `mouse-drag-secondary' + + (easy-menu-add lego-shell-menu lego-shell-mode-map) + + (and running-xemacs (define-key lego-shell-mode-map + [button3] 'lego-shell-menu)) + + (setq font-lock-keywords lego-shell-font-lock-keywords-1) +) + (provide 'lego) @@ -34,32 +34,34 @@ (list 'make-variable-buffer-local (list 'quote var)) (list 'defvar var 'nil)) -;; These have to be supplied to configure the mode properly +;; These should be set before proof-config-done is called (deflocal proof-terminal-char) +(make-local-hook 'proof-pre-shell-start-hook) +(make-local-hook 'proof-post-shell-start-hook) + +(deflocal proof-comment-start) +(deflocal proof-comment-end) + +;; these should be set in proof-shell-start-hook + (deflocal proof-shell-prog-name) (deflocal proof-shell-process-name) +(deflocal proof-shell-buffer-name) (deflocal proof-shell-prompt-pattern) (deflocal proof-shell-mode-is) -(deflocal proof-comment-start) -(deflocal proof-comment-end) - ;; Supply these if you want -(make-local-hook 'proof-shell-pre-display-hook) -(make-local-hook 'proof-shell-post-display-hook) (make-local-hook 'proof-shell-safe-send-hook) (make-local-hook 'proof-shell-exit-hook) ;; These get computed in proof-mode-child-config-done (deflocal proof-terminal-string) -(deflocal proof-shell-working-dir) (deflocal proof-re-end-of-cmd) (deflocal proof-re-term-or-comment) -(deflocal proof-shell-buffer-name) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bridging the emacs19/xemacs gulf ;; @@ -198,7 +200,13 @@ (goto-char point) (proof-find-end-of-command (if COUNT (+ 1 COUNT) 2))))) -(defun proof-shell-buffer () (get-buffer proof-shell-buffer-name)) +(defun proof-shell-process () + (and (stringp proof-shell-process-name) + (get-process proof-shell-process-name))) + +(defun proof-shell-buffer () + (and (stringp proof-shell-buffer-name) + (get-buffer proof-shell-buffer-name))) (defun proof-display-buffer (buffer) (let ((tmp-buffer (current-buffer))) @@ -221,10 +229,15 @@ (and (string-match proof-re-end-of-cmd string) (run-hooks 'proof-shell-safe-send-hook))) +(defun proof-interrupt-subjob () + (interactive) + (and (proof-shell-process) + (interrupt-process (proof-shell-process)))) + (defun proof-simple-send (string &optional silent) "send `string' to the PROOF PROCESS. If `silent' is enabled then `string' should not be echoed." - (or (get-process proof-shell-process-name) (proof-start-shell)) + (or (proof-shell-process) (proof-start-shell)) (let ((proof-buf (proof-shell-buffer))) (if proof-buf (save-excursion @@ -290,7 +303,6 @@ (defun proof-command (command) (run-hooks 'lego-shell-safe-send-hook) (let ((str (proof-append-terminator command))) - (insert str) (proof-simple-send str))) @@ -301,6 +313,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (defun proof-start-shell () + (run-hooks 'proof-pre-shell-start-hook) (let ((proof-buf (and proof-shell-process-name (proof-shell-buffer)))) (if (comint-check-proc proof-buf) () @@ -309,7 +322,6 @@ (setq proof-shell-prog-name (read-shell-command "Run process: " proof-shell-prog-name)))) - (setq proof-shell-working-dir default-directory) (or proof-shell-process-name (setq proof-shell-process-name (concat @@ -321,6 +333,7 @@ (proof-spawn-process proof-shell-prog-name proof-shell-process-name proof-shell-buffer-name) + (run-hooks 'proof-post-shell-start-hook) (message (format "Starting %s process... done." proof-shell-process-name))))) @@ -341,11 +354,8 @@ (setq comint-scroll-to-bottom-on-output t) (setq comint-input-sender 'proof-input-sender) (and running-emacs19 (setq comint-scroll-show-maximum-output t)) - - (run-hooks 'proof-shell-pre-display-hook) (proof-display-buffer buffer-name) (set-buffer buffer-name) - (run-hooks 'proof-shell-post-display-hook) ) (defun proof-shell-exit () @@ -372,11 +382,6 @@ (message (format "%s process terminated." proof-shell-process-name))))))) -(defun proof-interrupt-subjob () - "Send an interrupt signal to the PROOF process." - (interactive) (proof-simple-send "\C-q\C-c" t)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Active terminator minor mode ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -487,7 +492,8 @@ current command." (define-key proof-mode-map [(control c) (control e)] 'proof-find-end-of-command) (define-key proof-mode-map [(control c) (control j)] 'proof-send-line) -(define-key proof-mode-map [(control c) (control r)] 'proof-send-region) +(define-key proof-mode-map [(control c) r] 'proof-send-region) +(define-key proof-mode-map [(control c) (control c)] 'proof-interrupt-subjob) (define-derived-mode proof-shell-mode comint-mode "proof-shell" "Proof shell mode - not standalone" @@ -497,9 +503,7 @@ current command." ;; elegant mechanism for computing constants after the child has ;; configured. -(defun proof-mode-child-config-done () - - (setq proof-shell-buffer-name (concat "*" proof-shell-process-name "*")) +(defun proof-config-done () ;; calculate some strings and regexps for searching @@ -517,6 +521,13 @@ current command." (setq proof-re-term-or-comment (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) "\\|" (regexp-quote proof-comment-end))) + + (define-key proof-mode-map + (vconcat [(control c)] (vector proof-terminal-char)) + 'proof-active-terminator-minor-mode) + + (define-key proof-mode-map proof-terminal-char 'proof-active-terminator) + ) |