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

13 files changed, 184 insertions, 194 deletions

diff --git a/Makefile.devel b/Makefile.devel
index 48ab9786..a1e3317d 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -101,9 +101,18 @@ DISTINSTALLDIR=/export/local/share/elisp
 
 # Copied from distributed Makefile
 ELISP_DIRS=generic lego coq isa
+
+PWD=$(shell pwd)
+
+BYTECOMP = $(EMACS) -batch -q -no-site-file -eval '(setq load-path (append (list "$(PWD)/generic" "$(PWD)/lego" "$(PWD)/coq" "$(PWD)/isa") load-path))' -f batch-byte-compile
+
 EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
 ELC=$(EL:.el=.elc)
 
+.SUFFIXES:	.el .elc
+
+.el.elc:
+	$(BYTECOMP) $*.el
 
 FORCE:
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index ba5fc09b..e0ddba66 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -167,10 +167,10 @@
   (list
 
    ;; lambda binders
-   (list (coq-abstr-regexp "\\[" ":") 1 'proof-declaration-name-face)
+   (list (coq-abstr-regexp "\\[" ":") 1 ''proof-declaration-name-face)
 
    ;; Pi binders
-   (list (coq-abstr-regexp "(" ":") 1 'proof-declaration-name-face)
+   (list (coq-abstr-regexp "(" ":") 1 ''proof-declaration-name-face)
    
    ;; Kinds
    (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
@@ -181,31 +181,31 @@
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
 (defconst coq-save-command-regexp
-  (concat "^" (ids-to-regexp coq-keywords-save)))
+  (concat "^" (proof-ids-to-regexp coq-keywords-save)))
 (defconst coq-save-with-hole-regexp
-  (concat "\\(" (ids-to-regexp coq-keywords-save)
+  (concat "\\(" (proof-ids-to-regexp coq-keywords-save)
 	  "\\)\\s-+\\(" coq-id "\\)\\s-*\."))
 (defconst coq-goal-command-regexp
-  (concat "^" (ids-to-regexp coq-keywords-goal)))
+  (concat "^" (proof-ids-to-regexp coq-keywords-goal)))
 (defconst coq-goal-with-hole-regexp
-  (concat "\\(" (ids-to-regexp coq-keywords-goal)
+  (concat "\\(" (proof-ids-to-regexp coq-keywords-goal)
 	  "\\)\\s-+\\(" coq-id "\\)\\s-*:"))
 (defconst coq-decl-with-hole-regexp
-  (concat "\\(" (ids-to-regexp coq-keywords-decl)
+  (concat "\\(" (proof-ids-to-regexp coq-keywords-decl)
 	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
 (defconst coq-defn-with-hole-regexp
-  (concat "\\(" (ids-to-regexp coq-keywords-defn)
+  (concat "\\(" (proof-ids-to-regexp coq-keywords-defn)
 	  "\\)\\s-+\\(" coq-id "\\)\\s-*[:[]"))
 
 (defvar coq-font-lock-keywords-1
    (append
     coq-font-lock-terms
     (list
-     (cons (ids-to-regexp coq-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp coq-tacticals) 'proof-tacticals-name-face)
+     (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face)
+     (cons (proof-ids-to-regexp coq-tacticals) ''proof-tacticals-name-face)
 
      (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)
-     (list coq-decl-with-hole-regexp 2 'proof-declaration-name-face)
+     (list coq-decl-with-hole-regexp 2 ''proof-declaration-name-face)
      (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
      (list coq-save-with-hole-regexp 2 'font-lock-function-name-face))))
 
diff --git a/coq/coq.el b/coq/coq.el
index 095e920d..b283446c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -66,7 +66,7 @@
 ;; ----- outline
 
 (defvar coq-outline-regexp
-  (ids-to-regexp 
+  (proof-ids-to-regexp 
 	   '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact"
 	   "Remark" "Record" "Inductive" "Definition")))
 
@@ -78,7 +78,7 @@
 (defconst coq-kill-goal-command "Abort.")
 (defconst coq-forget-id-command "Reset ")
 
-(defconst coq-undoable-commands-regexp (ids-to-regexp coq-tactics))
+(defconst coq-undoable-commands-regexp (proof-ids-to-regexp coq-tactics))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
@@ -135,7 +135,7 @@
       (concat "Undo " (int-to-string ct) proof-terminal-string))))
 
 (defconst coq-keywords-decl-defn-regexp
-  (ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
+  (proof-ids-to-regexp (append coq-keywords-decl coq-keywords-defn))
   "Declaration and definition regexp.")
 
 (defun coq-goal-command-p (str)
@@ -351,7 +351,7 @@
 	proof-save-with-hole-regexp coq-save-with-hole-regexp
 	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
 	proof-kill-goal-command coq-kill-goal-command
-	proof-commands-regexp (ids-to-regexp coq-keywords))
+	proof-commands-regexp (proof-ids-to-regexp coq-keywords))
 
   (coq-init-syntax-table)
 
diff --git a/doc/notes.txt b/doc/notes.txt
index bbd9ab16..ebed6181 100644
--- a/doc/notes.txt
+++ b/doc/notes.txt
@@ -130,6 +130,14 @@ theory, see [Reference to Isabelle manual]
 
 **********
 
+Support for font-lock under FSF Emacs 20.2
+
+To automatically switch on fontification, set
+
+ (add-hook 'lego-mode-hooks 'turn-on-font-lock)
+                          ^
+
+
 *****************************************************************
 
 Notes for writing a paper describing Proof General
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
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index aabb0d4d..8a59c076 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -110,10 +110,10 @@
   (list
    ;; lambda binders
    (list (concat "\%\\s-*\\(" isa-ids "\\)\\.") 1
-	 'proof-declaration-name-face)
+	 ''proof-declaration-name-face)
 
    ;; Pi binders
-   (list (isa-abstr-regexp "(" ":") 1 'proof-declaration-name-face)
+   (list (isa-abstr-regexp "(" ":") 1 ''proof-declaration-name-face)
    
    ;; Kinds
    (cons (concat "\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\s-*\\(("
@@ -121,37 +121,37 @@
   "*Font-lock table for Isa terms.")
 
 (defconst isa-save-command-regexp
-  (concat "^" (ids-to-regexp isa-keywords-save)))
+  (concat "^" (proof-ids-to-regexp isa-keywords-save)))
 (defconst isa-save-with-hole-regexp
-  (concat "\\(" (ids-to-regexp isa-keywords-save)
+  (concat "\\(" (proof-ids-to-regexp isa-keywords-save)
 	  "\\)\\s-+\\(" isa-id "\\)\\s-*\."))
 
 ;; FIXME: where?
 (defcustom isa-goal-command-regexp
-  (concat "^" (ids-to-regexp isa-keywords-goal))
+  (concat "^" (proof-ids-to-regexp isa-keywords-goal))
   "Regular expression used to match a goal."
   :type 'regexp
   :group 'isabelle-config)
 
 (defconst isa-goal-with-hole-regexp
-  (concat "\\(" (ids-to-regexp isa-keywords-goal)
+  (concat "\\(" (proof-ids-to-regexp isa-keywords-goal)
 	  "\\)\\s-+\\(" isa-id "\\)\\s-*:"))
 (defconst isa-decl-with-hole-regexp
-  (concat "\\(" (ids-to-regexp isa-keywords-decl)
+  (concat "\\(" (proof-ids-to-regexp isa-keywords-decl)
 	  "\\)\\s-+\\(" isa-ids "\\)\\s-*:"))
 (defconst isa-defn-with-hole-regexp
-  (concat "\\(" (ids-to-regexp isa-keywords-defn)
+  (concat "\\(" (proof-ids-to-regexp isa-keywords-defn)
 	  "\\)\\s-+\\(" isa-id "\\)\\s-*[:[]"))
 
 (defvar isa-font-lock-keywords-1
    (append
     isa-font-lock-terms
     (list
-     (cons (ids-to-regexp isa-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp isa-tacticals) 'proof-tacticals-name-face)
+     (cons (proof-ids-to-regexp isa-keywords) 'font-lock-keyword-face)
+     (cons (proof-ids-to-regexp isa-tacticals) ''proof-tacticals-name-face)
 
      (list isa-goal-with-hole-regexp 2 'font-lock-function-name-face)
-     (list isa-decl-with-hole-regexp 2 'proof-declaration-name-face)
+     (list isa-decl-with-hole-regexp 2 ''proof-declaration-name-face)
      (list isa-defn-with-hole-regexp 2 'font-lock-function-name-face)
      (list isa-save-with-hole-regexp 2 'font-lock-function-name-face))))
 
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index f3a8f767..34608afb 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -64,7 +64,7 @@
 
    ; lambda binders
      (list (lego-decl-defn-regexp "[:|?]") 1
-	   'proof-declaration-name-face)
+	   ''proof-declaration-name-face)
 
      ; let binders
      (list lego-definiendum-alternative-regexp 1 'font-lock-function-name-face)
@@ -72,7 +72,7 @@
 
      ; Pi and Sigma binders
      (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
-	   'proof-declaration-name-face)
+	   ''proof-declaration-name-face)
    
      ;; Kinds
      (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
@@ -82,12 +82,12 @@
 ;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
 ;; it might be safer to append "\\s-*:".
 (defconst lego-goal-with-hole-regexp
-  (concat "\\(" (ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)")
+  (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)")
   "Regular expression which matches an entry in `lego-keywords-goal'
   and the name of the goal.") 
 
 (defconst lego-save-with-hole-regexp
-  (concat "\\(" (ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
+  (concat "\\(" (proof-ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
   "Regular expression which matches an entry in
   `lego-keywords-save' and the name of the goal.")
 
@@ -95,8 +95,8 @@
    (append
     lego-font-lock-terms
     (list
-     (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face)
-     (cons (ids-to-regexp lego-tacticals) 'proof-tacticals-name-face)
+     (cons (proof-ids-to-regexp lego-keywords) 'font-lock-keyword-face)
+     (cons (proof-ids-to-regexp lego-tacticals) ''proof-tacticals-name-face)
      (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
      (list lego-save-with-hole-regexp 2 'font-lock-function-name-face))))
      
diff --git a/lego/lego.el b/lego/lego.el
index 3674979d..a1c5b234 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -135,15 +135,15 @@
   "*Regular expression indicating that the proof has been completed.")
 
 (defvar lego-save-command-regexp
-  (concat "^" (ids-to-regexp lego-keywords-save)))
+  (concat "^" (proof-ids-to-regexp lego-keywords-save)))
 (defvar lego-goal-command-regexp
-  (concat "^" (ids-to-regexp lego-keywords-goal)))
+  (concat "^" (proof-ids-to-regexp lego-keywords-goal)))
 
 (defvar lego-kill-goal-command "KillRef;")
 (defvar lego-forget-id-command "Forget ")
 
 (defvar lego-undoable-commands-regexp
-  (ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
+  (proof-ids-to-regexp '("Dnf" "Refine" "Intros" "intros" "Next" "Normal"
   "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption"
   "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" "ImpI"
   "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed"
@@ -155,7 +155,7 @@
 
 (defvar lego-outline-regexp
   (concat "[[*]\\|"
-	  (ids-to-regexp 
+	  (proof-ids-to-regexp 
 	   '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive"
      "Unfreeze"))))
 
@@ -184,6 +184,7 @@
   (define-derived-mode lego-response-mode proof-response-mode
     "LEGOResp" nil
     (setq font-lock-keywords lego-font-lock-terms)
+    (lego-init-syntax-table)
     (proof-response-config-done)))
   
 (define-derived-mode lego-pbp-mode pbp-mode
@@ -410,7 +411,7 @@
 	proof-save-with-hole-regexp lego-save-with-hole-regexp
 	proof-goal-with-hole-regexp lego-goal-with-hole-regexp
 	proof-kill-goal-command lego-kill-goal-command
-	proof-commands-regexp (ids-to-regexp lego-commands))
+	proof-commands-regexp (proof-ids-to-regexp lego-commands))
 
   (lego-init-syntax-table)
 
@@ -537,6 +538,7 @@ We assume that module identifiers coincide with file names."
   (setq pbp-change-goal "Next %s;"
 	pbp-error-regexp lego-error-regexp)
   (setq font-lock-keywords lego-font-lock-terms)
+  (lego-init-syntax-table)
   (proof-goals-config-done))
   
 
diff --git a/todo b/todo
index 1d38d14e..83a19f08 100644
--- a/todo
+++ b/todo
@@ -382,8 +382,10 @@ C Improve legotags. I cannot handle lists e.g., with
 * Here are things to be done to Coq mode
 ========================================
 
+B Ensure that coq.el byte-compiles cleanly (1h)
+
 D set proof-commands-regexp to support indentation for commands
-						    (10min hhg)
+						    (10min)
 
 D Add Patrick Loiseleur's commands to search for vernac or ml files.
 
@@ -399,7 +401,7 @@ B Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
 D Proof-by-Pointing (10h hhg)
 
 B Add coq-add-tactic with a tactic name, which adds that tactic to the 
-  undoable tactics and to the font-lock. (2h hhg)
+  undoable tactics and to the font-lock. (2h)
 
 C Improve coqtags. I cannot handle lists e.g., with 	
 
@@ -436,11 +438,10 @@ X Manage multiple proofs (markers in possibly different buffers)
 * FSF Emacs
 ===========
 
-B According to the documentation of font-lock for Emacs 20.2, it
-  should suffice to set (add-hook 'lego-mode-hook 'turn-on-font-lock)
-  but this doesn't seem to work. Perhaps define-derived-mode doesn't
-  set up lego-mode correctly? (1h tms)
-
+C `proof-zap-commas-region' does not work for Emacs 20.2 on
+  lego/example.l . On *initially* fontifying the buffer,
+  commas are not zapped. However, when entering text, commata are
+  zapped correctly. (2h)
 
 * Release
 =========