diff options
| -rw-r--r-- | etc/junk.el | 10 | ||||
| -rw-r--r-- | generic/proof-config.el | 4 | ||||
| -rw-r--r-- | generic/proof-script.el | 16 | ||||
| -rw-r--r-- | generic/proof-shell.el | 83 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 3 | ||||
| -rw-r--r-- | generic/proof-x-symbol.el | 47 | ||||
| -rw-r--r-- | generic/proof.el | 98 | ||||
| -rw-r--r-- | isa/isa-syntax.el | 2 |
8 files changed, 184 insertions, 79 deletions
diff --git a/etc/junk.el b/etc/junk.el index 46da7f0c..d16b7f61 100644 --- a/etc/junk.el +++ b/etc/junk.el @@ -57,3 +57,13 @@ arrive." ; (setq font-lock-defaults '(proof-font-lock-defaults))))) ; (put major-mode 'font-lock-defaults (list flks))))) + + +;; dump str to buffer ug for testing. +(defun ugit (str) + (save-excursion + (set-buffer (get-buffer-create "ug")) + (goto-char (point-max)) + (insert str) + (newline) + (newline))) diff --git a/generic/proof-config.el b/generic/proof-config.el index 7703c08e..4ec803ee 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -121,6 +121,10 @@ inside your Emacs." :set 'proof-set-bool :group 'proof-user-options) +(defcustom proof-output-fontify-enable t + "*Whether to fontify output from the proof assistant." + :type 'boolean + :group 'proof-user-options) (defcustom proof-strict-read-only ;; For FSF Emacs, strict read only is buggy when used in diff --git a/generic/proof-script.el b/generic/proof-script.el index 5805d0e6..535cf0a8 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2282,20 +2282,8 @@ finish setup which depends on specific proof assistant configuration." ;; ;; Fontlock. - ;; - ;; At the moment, the specific code hacks font-lock-keywords. - ;; Here we use the value there to hack font-lock-defaults, which - ;; is used by font-lock to set font-lock-keywords from again!! - ;; Yuk. - ;; Previously, font-lock-keywords was used directly as a setting - ;; for the defaults. This has a bad interaction with x-symbol - ;; which edits font-lock-keywords and loses the setting. - ;; So we make a copy of it in a new variable. - ;; - (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF? - (make-local-variable 'proof-font-lock-defaults) - (setq proof-font-lock-defaults font-lock-keywords) - (setq font-lock-defaults '(proof-font-lock-defaults)) + ;; + (proof-font-lock-configure-defaults) ;; FIXME (da): zap commas support is too specific, should be enabled ;; by each proof assistant as it likes. diff --git a/generic/proof-shell.el b/generic/proof-shell.el index f6a23800..2b948fa2 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -687,8 +687,8 @@ This is a list of tuples of the form (TYPE . STRING). type is either (insert string) (insert (substring out 0 op))) - ;; Display special characters - (proof-x-symbol-decode-region (point-min) (point-max)) + ;; Get fonts and characters right + (proof-fontify-region (point-min) (point-max)) (proof-display-and-keep-buffer proof-goals-buffer (point-min)) @@ -760,6 +760,24 @@ This is a list of tuples of the form (TYPE . STRING). type is either (incf ip)) (substring out 0 op))) +(defun proof-shell-strip-eager-annotation-specials (string) + "Strip special eager annotations from STRING, returning cleaned up string. +The input STRING should be annotated with expressions matching +proof-shell-eager-annotation-start and eager-annotation-end. +We only strip specials from the annotations." + (let* ((mstart (progn + (string-match proof-shell-eager-annotation-start string) + (match-end 0))) + (mend (string-match proof-shell-eager-annotation-end string)) + (msg (substring string mstart mend)) + (strtan (substring string 0 mstart)) + (endan (substring string mend))) + (concat + (proof-shell-strip-special-annotations strtan) + msg + (proof-shell-strip-special-annotations endan)))) + + (defun proof-shell-handle-output (start-regexp end-regexp append-face) "Displays output from `proof-shell-buffer' in `proof-response-buffer'. The region in `proof-shell-buffer begins with the first match @@ -780,7 +798,7 @@ Returns the string (with faces) in the specified region." (setq string (if proof-shell-leave-annotations-in-output (buffer-substring start end) - (proof-shell-strip-special-annotations + (proof-shell-strip-special-annotations (buffer-substring start end))))) ;; Erase if need be, and erase next time round too. (proof-shell-maybe-erase-response t nil) @@ -822,7 +840,7 @@ See the documentation for `proof-shell-delayed-output' for further details." (proof-shell-maybe-erase-response t nil) (setq pos (point)) (insert str) - (proof-x-symbol-decode-region pos (point)) + (proof-fontify-region pos (point)) (proof-display-and-keep-buffer proof-response-buffer))) ;; ;; 2. Text to be inserted in goals buffer @@ -874,7 +892,7 @@ Then we call `proof-shell-handle-error-hook'. " (set-buffer proof-goals-buffer) (erase-buffer) (insert (cdr proof-shell-delayed-output)) - (proof-x-symbol-decode-region (point-min) (point-max)) + (proof-fontify-region (point-min) (point-max)) (proof-display-and-keep-buffer proof-goals-buffer))) ;; This prevents problems if the user types in the @@ -1220,13 +1238,9 @@ Assume proof-script-buffer is active." (defun proof-shell-process-urgent-message (message) "Analyse urgent MESSAGE for various cases. Cases are: included file, retracted file, cleared response buffer, or -if none of these apply, display it." - (save-excursion - (set-buffer (get-buffer-create "ug")) - (goto-char (point-max)) - (insert "Hello!") - (insert message) - (newline)) +if none of these apply, display it. +MESSAGE should be a string annotated with +proof-shell-eager-annotation-start, proof-shell-eager-annotation-end." (cond ;; Is the prover processing a file? ;; FIXME da: this interface is quite restrictive: might be @@ -1329,9 +1343,14 @@ if none of these apply, display it." ;; Don't bother remove the window for the response buffer ;; because we're about to put a message in it. (proof-shell-maybe-erase-response nil nil) - (proof-shell-message message) - (proof-response-buffer-display message - 'proof-eager-annotation-face)))) + (let ((stripped (proof-shell-strip-special-annotations message))) + (if (< 100 (length stripped)) ;; approx test for multi-line msg + (proof-shell-message stripped)) + (proof-response-buffer-display + (if proof-shell-leave-annotations-in-output + message + stripped) + 'proof-eager-annotation-face))))) (defvar proof-shell-urgent-message-marker nil "Marker in proof shell buffer pointing to end of last urgent message.") @@ -1360,8 +1379,7 @@ This is a subroutine of proof-shell-filter." (save-excursion (setq lastend end) (proof-shell-process-urgent-message - (proof-shell-strip-special-annotations - (buffer-substring start end)))))) + (buffer-substring start end))))) ;; Set the marker to the (character after) the end of the last ;; message found, if any. Must take care to keep the marker ;; behind the process marker otherwise no output is seen! @@ -1510,7 +1528,7 @@ however, are always processed; hence their name)." ;; expensive; but perhaps we could cut and paste ;; from here to the goals buffer to ;; avoid duplicating effort? - ;; (proof-x-symbol-decode-region startpos (point)) + ;; (proof-fontify-region startpos (point)) (setq string (buffer-substring startpos (point))) (goto-char (point-max)) (proof-shell-filter-process-output string))))))))) @@ -1688,40 +1706,19 @@ before and after sending the command." (cons proof-general-name proof-shell-menu)) - -(defun proof-font-lock-configure-defaults () - "Set defaults for font-lock based on current font-lock-keywords." - ;; setting font-lock-defaults explicitly is required by FSF Emacs - ;; 20.2's version of font-lock - (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF? - (make-local-variable 'proof-font-lock-defaults) - (setq proof-font-lock-defaults font-lock-keywords) - (setq font-lock-defaults '(proof-font-lock-defaults)) - ;; Turn on fontification only if the user has configured it - ;; everywhere in general. - (if font-lock-auto-fontify - (turn-on-font-lock))) - (defun proof-goals-config-done () "Initialise the goals buffer after the child has been configured." (save-excursion (set-buffer proof-goals-buffer) (proof-font-lock-configure-defaults) - ;; Turn off the display of annotations here - (proof-shell-dont-show-annotations) - ;; Maybe turn on x-symbols - (proof-x-symbol-mode))) + (proof-x-symbol-configure))) (defun proof-response-config-done () "Initialise the response buffer after the child has been configured." (save-excursion (set-buffer proof-response-buffer) (proof-font-lock-configure-defaults) - ;; Turn off the display of annotations here - (proof-shell-dont-show-annotations) - ;; Maybe turn on x-symbols - (proof-x-symbol-mode))) - + (proof-x-symbol-configure))) (defun proof-shell-config-done () "Initialise the specific prover after the child has been configured. @@ -1745,9 +1742,9 @@ processing." ;; Send intitialization command and wait for it to be ;; processed. Also ensure that proof-action-list is ;; initialised. + (setq proof-action-list nil) (if proof-shell-init-cmd - (proof-shell-invisible-command proof-shell-init-cmd t) - (setq proof-action-list nil)) + (proof-shell-invisible-command proof-shell-init-cmd t)) ;; Configure for x-symbol (proof-x-symbol-shell-config)))) diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 37819d8b..f5c7668b 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -96,6 +96,9 @@ Default is comma separated, or SEPREGEXP if set." ;;FIXME: Under FSF Emacs 20.2, when initially fontifying the buffer, ;; commas are not zapped. +;; +;; FIXME da: this should be more specific!! +;; (defun proof-zap-commas-region (start end &optional length) "Remove the face of all `,' within the region (START,END). The optional argument LENGTH has no effect. It is required so that we diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index 697956e3..0d15d18e 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -66,9 +66,10 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol")) ((not (condition-case () (require xs-feature-sym) ;; NB: lose all errors! (t (featurep xs-feature-sym)))) - (format - "Proof General: for x-symbol support, you must provide a library %s.el" - xs-feature)) + (funcall error-or-warn + (format + "Proof General: for x-symbol support, you must provide a library %s.el" + xs-feature))) (t ;; ;; We've got everything we need! So initialize. @@ -124,8 +125,7 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol")) ;;;###autoload (defun proof-x-symbol-enable () "Turn on or off support for x-symbol, initializing if necessary." - (if ;(and proof-x-symbol-enable (not proof-x-symbol-initialized)) - proof-x-symbol-enable + (if (and proof-x-symbol-enable (not proof-x-symbol-initialized)) (progn (setq proof-x-symbol-enable nil) ; assume failure! (proof-x-symbol-initialize 'giveerrors) @@ -138,8 +138,9 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol")) (proof-customize-toggle proof-x-symbol-enable)) (defun proof-x-symbol-decode-region (start end) - "Call (x-symbol-decode-region START END), if x-symbol support is enabled." - (if proof-x-symbol-enable + "Call (x-symbol-decode-region A Z), if x-symbol support is enabled. +This converts tokens in the region into X-Symbol characters." + (if (and proof-x-symbol-enable) (x-symbol-decode-region start end))) (defun proof-x-symbol-encode-shell-input () @@ -166,6 +167,8 @@ A value for proof-shell-insert-hook." (save-excursion ; needed or point moves: why? (if proof-x-symbol-initialized (progn + ;; Buffers which have XS minor mode toggled always keep + ;; x-symbol-language set. (setq x-symbol-language proof-assistant-symbol) (if (eq x-symbol-mode (not proof-x-symbol-enable)) ;; toggle x-symbol-mode @@ -180,23 +183,39 @@ A value for proof-shell-insert-hook." ;; contents) have changed. I think x-symbol ;; ought to do this really! (font-lock-fontify-buffer))))))) - + +(defun proof-x-symbol-configure () + "Configure the current buffer for X-Symbol." + (if proof-x-symbol-enable + (setq x-symbol-language proof-assistant-symbol) + (setq x-symbol-language nil))) + (defun proof-x-symbol-mode-all-buffers () - "Activate/deactivate x-symbol mode in all Proof General buffers. + "Activate/deactivate x-symbols in all Proof General buffers. A subroutine of proof-x-symbol-enable." + ;; Shell has its own routine (proof-with-current-buffer-if-exists proof-shell-buffer (proof-x-symbol-shell-config)) + ;; Response and goals buffer are fontified/decoded + ;; manually in the code. + (proof-with-current-buffer-if-exists + proof-goals-buffer + (proof-x-symbol-configure) + (proof-fontify-buffer)) + (proof-with-current-buffer-if-exists + proof-response-buffer + (proof-x-symbol-configure) + (proof-fontify-buffer)) + ;; Script buffers are in x-symbol mode (let - ((bufs (append - (list proof-goals-buffer proof-response-buffer) - (proof-buffers-in-mode proof-mode-for-script)))) + ((bufs (proof-buffers-in-mode proof-mode-for-script))) (while bufs ;; mapcar doesn't work with macros - (proof-with-current-buffer-if-exists (car bufs) - (proof-x-symbol-mode)) + (with-current-buffer (car bufs) (proof-x-symbol-mode)) (setq bufs (cdr bufs))))) + ;; #### autoload (defun proof-x-symbol-shell-config () "Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil. diff --git a/generic/proof.el b/generic/proof.el index 95e70c07..a1bc4586 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -82,6 +82,9 @@ (autoload 'proof-x-symbol-mode "proof-x-symbol" "Turn on or off x-symbol mode in the current buffer.") +(autoload 'proof-x-symbol-configure "proof-x-symbol" + "Configure the current buffer for X-Symbol.") + ;;; ;;; Global variables ;;; @@ -141,7 +144,6 @@ read.") "End-of-line string for proof process.") - ;;; ;;; Utilities/macros used in several files (-> proof-utils) ;;; @@ -220,13 +222,91 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding kbl)) ;; ----------------------------------------------------------------- +;; Managing font-lock +;; + +;; Buffers which are output only are *not* kept in special minor +;; modes font-lock-mode (or x-symbol-mode). In case the user +;; doesn't want fontification we have a user option, +;; proof-fontify-output. + +(deflocal proof-font-lock-defaults nil + "Default value for font-lock-keywords in this buffer. +We set font-lock-defaults to '(proof-font-lock-defaults) for +compatibility with X-Symbol, which may hack proof-font-lock-defaults +with extra patterns (in non-mule mode).") + +(defun proof-font-lock-configure-defaults () + "Set defaults for font-lock based on current font-lock-keywords." + ;; + ;; At the moment, the specific assistant code hacks + ;; font-lock-keywords. Here we use that value to hack + ;; font-lock-defaults, which is used by font-lock to set + ;; font-lock-keywords from again!! Yuk. + ;; + ;; Previously, 'font-lock-keywords was used directly as a setting + ;; for the defaults. This has a bad interaction with x-symbol which + ;; edits font-lock-keywords and loses the setting. So we make a + ;; copy of it in a new local variable, proof-font-lock-defaults. + ;; + (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF? + (setq proof-font-lock-defaults font-lock-keywords) + ;; Setting font-lock-defaults explicitly is required by FSF Emacs + ;; 20.2's version of font-lock in any case. + (setq font-lock-defaults '(proof-font-lock-defaults))) + + +(defun proof-fontify-region (start end) + "Fontify and decode X-Symbols in region START...END. +Fontifies according to the buffer's font lock defaults. +Uses proof-x-symbol-decode to decode tokens if x-symbol is present. + +If proof-shell-leave-annotations-in-output is set, remove characters +with top bit set after fontifying so they can be used for +fontification. + +Returns new END value." + ;; We fontify first because decoding changes char positions. + ;; It's okay because x-symbol-decode works even without font lock. + ;; Possible disadvantage is that font lock patterns can't refer + ;; to X-Symbol characters. Probably they shouldn't! + (narrow-to-region start end) + (if proof-output-fontify-enable + (let ((font-lock-keywords proof-font-lock-defaults)) + (font-lock-fontify-region start end) + ;; FIXME: this should be optional, really. + (proof-zap-commas-region start end))) + (if proof-shell-leave-annotations-in-output + ;; Remove special characters that were used for font lock, + ;; so cut and paste works from here. + (let ((p (point))) + (goto-char start) + (while (< (point) (point-max)) + (forward-char) + (unless (< (char-to-int (char-before (point))) 128) + (delete-char -1))) + (goto-char p))) + (proof-x-symbol-decode-region start (point-max)) + (prog1 (point-max) + (widen))) + +;; FIXME todo: add toggle for fontify region which turns it on/off +;; (maybe). + +(defun proof-fontify-buffer () + "Call proof-fontify-region on whole buffer." + (proof-fontify-region (point-min) (point-max))) + + + +;; ----------------------------------------------------------------- ;; Display functions +;; + -;; FIXME: this function should be combined with -;; proof-shell-maybe-erase-response-buffer. Should allow -;; face of nil for unfontified output. (defun proof-response-buffer-display (str &optional face) "Display STR with FACE in response buffer and return fontified STR." + (ugit str) ;; FIXME: debug! (let (start end) (with-current-buffer proof-response-buffer ;; da: I've moved newline before the string itself, to match @@ -236,10 +316,14 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding (newline) (setq start (point)) (insert str) - (proof-x-symbol-decode-region start (point)) - (setq end (point-max)) + (setq end (proof-fontify-region start (point))) + ;; This is why we can't keep the buffer in font-lock + ;; minor mode: it destroys this hacky property as soon + ;; as it's made! (if face (font-lock-append-text-property start end 'face face)) - (buffer-substring start end)))) + ;; This returns the decorated string, but it doesn't appear + ;; decorated in the minibuffer, unfortunately. + (buffer-substring start (point-max))))) ;; FIXME da: this window dedicated stuff is a real pain and I've ;; spent ages inserting workarounds. Why do we want it?? diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 767df53a..c18ea0a7 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -297,7 +297,7 @@ (cons (concat "\353\\?'" isa-idx "\350") 'isabelle-tvar-name-face) (cons (concat "\354" isa-id "\350") 'isabelle-free-name-face) (cons (concat "\355" isa-id "\350") 'isabelle-bound-name-face) - (cons (concat "\356" "\\?" isa-idx "\350") 'isabelle-var-name-face) + (cons (concat "\356\\?" isa-idx "\350") 'isabelle-var-name-face) (cons (concat "\357" isa-idx "\350") 'proof-declaration-name-face) ) "*Font-lock table for Isabelle terms.") |