o added support for byte-compilation

o removed hhg tags in todo
o fixed font-lock for FSF Emacs 20.2
o ensured that goals buffer is updated for longer queues
o fixed a bug in proof-universal-keys-only-mode

5 files changed, 120 insertions, 150 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 9fcb13ec..686f6a98 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -124,7 +124,10 @@ If ignore, point is never moved after toolbar movement commands."
       :bold t))
     (t				
      (:italic t :bold t)))
-  "*Face for declaration names in proof scripts."
+  "*Face for declaration names in proof scripts.
+
+Don't forget to *double* quote this face for font-lock. FSF Emacs
+20.2's version only supports *expressions* for faces."
   :group 'proof-faces)
 
 (defface proof-tacticals-name-face
@@ -134,7 +137,10 @@ If ignore, point is never moved after toolbar movement commands."
      (:foreground "orchid"))
     (t				
      (bold t)))
-  "*Face for names of tacticals in proof scripts."
+  "*Face for names of tacticals in proof scripts.
+
+Don't forget to *double* quote this face for font-lock. FSF Emacs
+20.2's version only supports *expressions* for faces."
   :group 'proof-faces)
 
 (defface proof-error-face 
@@ -692,7 +698,10 @@ where `k' is a keybinding (vector) and `f' the designated function."
   :type 'sexp
   :group 'proof-general-internals)
 
-
+(defcustom proof-window-dedicated-p t
+  "Flag whether response and goals buffers have dedicated windows."
+  :type 'boolean
+  :group 'proof-general-internals)
 
 ;;; 
 ;;; FIXME: unsorted below here
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f4b31772..f21dec99 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -428,25 +428,11 @@ Returns the string (with faces) in the specified region."
       (set-buffer proof-shell-buffer)
       (goto-char (point-max))
       (setq start (search-backward-regexp start-regexp))
-      (save-excursion (setq end (- (search-forward-regexp end-regexp)
-				   (length (match-string 0)))))
+      (setq end (- (search-forward-regexp end-regexp)
+				   (length (match-string 0))))
       (setq string
-	    (proof-shell-strip-annotations (buffer-substring start end)))
-      (set-buffer proof-response-buffer)
-      (goto-char (point-max))
-      (newline)
-      (setq start (point-max))
-      (insert string)
-      (setq end (+ start (length string)))
-      ;; FIXME tms: FSF Emacs 20.2 problems
-      ;; This doesn't work with FSF Emacs 20.2's version of Font-lock
-      ;; because there are no known keywords in the process buffer
-      ;; Never mind. In a forthcoming version, the process buffer will
-      ;; not be tampered with. Fontification will take place in a
-      ;; separate response buffer.
-      (font-lock-fontify-region start end)
-      (font-lock-append-text-property start end 'face append-face)
-      (buffer-substring start end))))
+	    (proof-shell-strip-annotations (buffer-substring start end))))
+    (proof-response-buffer-display string append-face)))
 
 (defun proof-shell-handle-delayed-output ()
   "Display delayed output. 
@@ -456,11 +442,11 @@ See the documentation fo `proof-shell-delayed-output' for furter details."
     (cond 
      ((eq ins 'insert)
       (setq str (proof-shell-strip-annotations str))
-      (save-excursion
+      (save-current-buffer
 	(set-buffer proof-response-buffer)
 	(erase-buffer)
-	(insert str))
-      (proof-display-and-keep-buffer proof-response-buffer))
+	(insert str)
+	(proof-display-and-keep-buffer proof-response-buffer)))
      ((eq ins 'analyse)
       (proof-shell-analyse-structure str))
      (t (assert nil))))
@@ -491,8 +477,19 @@ See the documentation fo `proof-shell-delayed-output' for furter details."
 
 (defun proof-shell-handle-error (cmd string)
   "React on an error message triggered by the prover.
+We first flush unprocessed goals to the goals buffer.
 The error message is displayed in the `proof-response-buffer'. Then,
 we call `proof-shell-handle-error-hook'. "
+
+  ;; flush goals
+  (or (equal proof-shell-delayed-output (cons 'insert "Done."))
+      (save-current-buffer
+	(set-buffer proof-pbp-buffer)
+	(erase-buffer)
+	(insert (proof-shell-strip-annotations 
+		   (cdr proof-shell-delayed-output)))
+	(proof-display-and-keep-buffer proof-pbp-buffer)))
+
     ;; We extract all text between text matching
     ;; `proof-shell-error-regexp' and the following prompt.
     ;; Alternatively one could higlight all output between the
@@ -504,7 +501,7 @@ we call `proof-shell-handle-error-hook'. "
   (proof-shell-handle-output
    proof-shell-error-regexp proof-shell-annotated-prompt-regexp
    'proof-error-face)
-  (save-excursion (proof-display-and-keep-buffer proof-response-buffer)
+  (save-current-buffer (proof-display-and-keep-buffer proof-response-buffer)
 		  (beep)
 
 		  ;; unwind script buffer
@@ -573,7 +570,7 @@ assistant."
    ((and proof-shell-abort-goal-regexp
 	 (string-match proof-shell-abort-goal-regexp string))
     (proof-clean-buffer proof-pbp-buffer)
-   (setq proof-shell-delayed-output (cons 'insert "\n\nAborted"))
+   (setq proof-shell-delayed-output (cons 'insert "\nAborted\n"))
     ())
 	 
    ((string-match proof-shell-proof-completed-regexp string)
@@ -871,7 +868,7 @@ how far we've got."
 					     (point)))
 	      (goto-char (point-max))	; da: assumed to be after a prompt?
 	      (setq cmd (nth 1 (car proof-action-list)))
-	      (save-excursion
+	      (save-current-buffer
 		;; 
 		(setq res (proof-shell-process-output cmd string))
 		;; da: Added this next line to redisplay, for proof-toolbar
@@ -1020,7 +1017,7 @@ Annotations are characters 128-255."
 (define-derived-mode proof-universal-keys-only-mode fundamental-mode
     proof-mode-name "Universal keymaps only"
     (suppress-keymap proof-universal-keys-only-mode-map 'all)
-    (proof-define-keys pbp-mode-map proof-universal-keys)))
+    (proof-define-keys proof-universal-keys-only-mode-map proof-universal-keys)))
 
 (eval-and-compile			; to define vars
 (define-derived-mode pbp-mode proof-universal-keys-only-mode
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 9ea7ee56..e9c2e707 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -8,9 +8,9 @@
 
 
 (require 'font-lock)
+(require 'proof-config)
 
-;;; FIXME: change this to proof-
-(defun ids-to-regexp (l)
+(defun proof-ids-to-regexp (l)
   "transforms a non-empty list of identifiers `l' into a regular
   expression matching any of its elements"
   (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|"))
@@ -35,60 +35,6 @@
   (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*"))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; font lock faces: declarations, errors, tacticals                 ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-
-;; FACES have been moved to proof-config.
-;; Old code left here while testing.
-
-;(defun proof-have-color ()
-;  "Do we have support for colour?"
-;  (or (and (fboundp 'device-class)
-;	   (eq (device-class (frame-device)) 'color))
-;      (and (fboundp 'x-display-color-p) (x-display-color-p))))
-
-;(defvar font-lock-declaration-name-face 
-;(progn 
-;  (cond 
-;   ((proof-have-color)
-;    (copy-face 'bold 'font-lock-declaration-name-face)
-
-;    ;; Emacs 19.28 compiles this down to
-;    ;; internal-set-face-1. This is not compatible with XEmacs
-;    (set-face-foreground
-;     'font-lock-declaration-name-face "chocolate"))
-;   (t (copy-face 'bold-italic 'font-lock-declaration-name-face)))))
-
-;;  (if running-emacs19
-;;      (setq font-lock-declaration-name-face
-;;	    (face-name 'font-lock-declaration-name-face))
-
-
-;(defvar font-lock-tacticals-name-face
-;(if (proof-have-color)
-;    (let ((face (make-face 'font-lock-tacticals-name-face)))
-;      (dont-compile
-;	(set-face-foreground face "MediumOrchid3"))
-;      face)
-;  (copy-face 'bold 'font-lock-tacticals-name-face)))
-
-;(defvar font-lock-error-face
-;  (let ((face (make-face 'font-lock-error-face)))
-;    (copy-face 'bold 'font-lock-error-face)
-;    (and (proof-have-color) (set-face-background face "salmon1"))
-;    face)
-;  "*The face for error messages.")
-
-;(defvar font-lock-eager-annotation-face
-;  (let ((face (make-face 'font-lock-eager-annotation-face)))
-;    (if (proof-have-color)
-;	(set-face-background face "lemon chiffon")
-;      (copy-face 'italic face))
-;    face)
-;  "*The face for urgent messages.")
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; A big hack to unfontify commas in declarations and definitions.  ;;
 ;; Useful for provers which have declarations of the form x,y,z:Ty  ;;
 ;; All that can be said for it is that the previous way of doing    ;;
@@ -98,7 +44,12 @@
 ;; Refontify the whole line, 'cos that's what font-lock-after-change
 ;; does.
 
-(defun proof-zap-commas-region (start end length)
+;;FIXME: Under FSF Emacs 20.2, when initially fontifying the buffer,
+;;       commas are not zapped. 
+(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
+may assign this function to `after-change-function'."
   (save-excursion
     (let 
 	((start (progn (goto-char start) (beginning-of-line) (point)))
@@ -106,13 +57,14 @@
       (goto-char start)
       (while (search-forward "," end t)
 	(if (memq (get-char-property (- (point) 1) 'face)
-		'(proof-declaration-name-face
-		  font-lock-function-name-face))
-	    (font-lock-remove-face (- (point) 1) (point))
+		(list 'proof-declaration-name-face
+		  'font-lock-function-name-face))
+	    (font-lock-unfontify-region (- (point) 1) (point))
 	    )))))
 
 (defun proof-zap-commas-buffer () 
-  (proof-zap-commas-region (point-min) (point-max) 0))
+  "Remove the face of all `,' in the current buffer."
+  (proof-zap-commas-region (point-min) (point-max)))
 
 (defun proof-unfontify-separator ()
      (make-local-variable 'after-change-functions)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 2686ccb3..7082cfbb 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -11,6 +11,7 @@
 ;;
 
 (require 'proof-script)
+(autoload 'proof-shell-live-buffer "proof-shell")
 
 (defconst proof-toolbar-default-button-list
   '(proof-toolbar-goal-button
diff --git a/generic/proof.el b/generic/proof.el
index 1d6580bc..4239e250 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -13,6 +13,13 @@
 ;; $Id$
 ;;
 
+(defmacro deflocal (var value &optional docstring)
+  "Define a buffer local variable VAR with default value VALUE."
+ (list 'progn
+   (list 'defvar var 'nil docstring)
+   (list 'make-variable-buffer-local (list 'quote var))
+   (list 'setq-default var value)))
+
 (require 'proof-site)			; site config
 
 (require 'proof-config)			; configuration variables
@@ -54,67 +61,8 @@
 (autoload 'proof-shell-available-p "proof-shell"
   "Returns non-nil if there is a proof shell active and available.")
 
-;;;
-;;; Utilities/macros used in several files  (proof-utils)
-;;;
-
-(defmacro deflocal (var value &optional docstring)
-  "Define a buffer local variable VAR with default value VALUE."
- (list 'progn
-   (list 'defvar var 'nil docstring)
-   (list 'make-variable-buffer-local (list 'quote var))
-   (list 'setq-default var value)))
-
-(defun proof-string-to-list (s separator) 
-  "Return the list of words in S separated by SEPARATOR."
-  (let ((end-of-word-occurence (string-match (concat separator "+") s)))
-    (if (not end-of-word-occurence)
-        (if (string= s "") 
-            nil
-          (list s))
-      (cons (substring s 0 end-of-word-occurence) 
-            (proof-string-to-list 
-             (substring s
-                        (string-match (concat "[^" separator "]")
-                                      s end-of-word-occurence)) separator)))))
-
-(defun proof-define-keys (map kbl)
-  "Adds keybindings KBL in MAP.
-The argument KBL is a list of tuples (k . f) where `k' is a keybinding
-(vector) and `f' the designated function."
-  (mapcar
-   (lambda (kbl)
-     (let ((k (car kbl)) (f (cdr kbl)))
-         (define-key map k f)))
-   kbl))
-
-(defun proof-response-buffer-display (str face)
-  "Display STR with FACE in response buffer."
-  (let ((start))
-    (save-excursion
-      (set-buffer proof-response-buffer)
-      (setq start (goto-char (point-max)))
-      (insert str)
-      ;; FIXME da: recurring bug here???
-      (if (string-match "XEmacs" emacs-version)
-	  (progn
-	    (font-lock-fontify-region start (point-max))
-	    (font-lock-append-text-property start (point-max) 'face face)))
-      ;; 
-      (insert "\n"))))
-
-(defun proof-display-and-keep-buffer (buffer)
-  "Display BUFFER and mark window as dedicated."
-  (display-buffer buffer)
-  (set-window-dedicated-p (get-buffer-window buffer) 'dedicated))
-
-(defun proof-clean-buffer (buffer)
-  "Erase buffer and hide from display."
-  (save-excursion
-    (set-buffer buffer)
-    (erase-buffer))
-  (delete-windows-on buffer))
-
+(autoload 'font-lock-fontify-region "font-lock")
+(autoload 'font-lock-append-text-property "font-lock")
 ;;;
 ;;; Global variables
 ;;;
@@ -162,5 +110,68 @@ The cdr of the list of corresponding file names is a subset of
 
 
 
+;;;
+;;; Utilities/macros used in several files  (proof-utils)
+;;;
+
+(defun proof-string-to-list (s separator) 
+  "Return the list of words in S separated by SEPARATOR."
+  (let ((end-of-word-occurence (string-match (concat separator "+") s)))
+    (if (not end-of-word-occurence)
+        (if (string= s "") 
+            nil
+          (list s))
+      (cons (substring s 0 end-of-word-occurence) 
+            (proof-string-to-list 
+             (substring s
+                        (string-match (concat "[^" separator "]")
+                                      s end-of-word-occurence)) separator)))))
+
+(defun proof-define-keys (map kbl)
+  "Adds keybindings KBL in MAP.
+The argument KBL is a list of tuples (k . f) where `k' is a keybinding
+(vector) and `f' the designated function."
+  (mapcar
+   (lambda (kbl)
+     (let ((k (car kbl)) (f (cdr kbl)))
+         (define-key map k f)))
+   kbl))
+
+(defun proof-response-buffer-display (str face)
+  "Display STR with FACE in response buffer and return fontified STR."
+  (let (start end)
+    (save-current-buffer
+      (set-buffer proof-response-buffer)
+      (setq start (goto-char (point-max)))
+      (insert str) (setq end (point))
+      (newline)
+      ;; FIXME tms: Make this work for FSF Emacs 20.2
+      (font-lock-fontify-region start end)
+      (font-lock-append-text-property start end 'face face)
+      (buffer-substring start end))))
+
+
+(defun proof-display-and-keep-buffer (buffer)
+  "Display BUFFER and mark window according to `proof-window-dedicated-p'."
+  (let ((window (get-buffer-window buffer 'visible)))
+    (save-selected-window
+    (display-buffer buffer)
+    (set-window-dedicated-p (get-buffer-window buffer)
+			    proof-window-dedicated-p)
+    (and window
+	 (progn (select-window window)
+		;; tms: I don't understand why the point in
+		;; proof-response-buffer is not at the end anyway.
+		;; Is there a superfluous save-excursion somewhere?
+		(goto-char (point-max))
+		(or (pos-visible-in-window-p) (recenter -1)))))))
+
+(defun proof-clean-buffer (buffer)
+  "Erase buffer and hide from display."
+  (save-excursion
+    (set-buffer buffer)
+    (erase-buffer))
+  (delete-windows-on buffer))
+
 (provide 'proof)
 ;; proof.el ends here