fixed minor bugs

6 files changed, 27 insertions, 15 deletions

diff --git a/coq/coq.el b/coq/coq.el
index b283446c..85431e50 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -6,16 +6,24 @@
 
 ;; $Id$
 
-(require 'proof)
+(require 'proof-script)
 (require 'coq-syntax)
 
+;; Spans are our abstraction of extents/overlays.
+(eval-and-compile
+  (cond ((fboundp 'make-extent) (require 'span-extent))
+	((fboundp 'make-overlay) (require 'span-overlay))))
+
+(eval-and-compile
+  (mapcar (lambda (f) (autoload f "proof-shell"))
+	    '(pbp-mode proof-shell-config-done))) 
 ;; FIXME: outline and info should be autoloaded.
 (require 'outline)
 (require 'info)
 
 ; Configuration
 
-(setq tag-always-exact t) ; Tags is unusable with Coq library otherwise:
+(setq tags-always-exact t) ; Tags is unusable with Coq library otherwise:
 
 (defcustom coq-tags "/usr/local/lib/coq/theories/TAGS"
   "the default TAGS table for the Coq library"
@@ -414,7 +422,7 @@
         proof-shell-end-goals-regexp proof-shell-annotated-prompt-regexp
         proof-shell-init-cmd nil
 	proof-analyse-using-stack t
-	proof-lift-global coq-lift-global)
+	proof-lift-global 'coq-lift-global)
 
   ;; The following hook is removed once it's called.
   (add-hook 'proof-shell-insert-hook 'coq-shell-init-hook nil t)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f21dec99..39c6208f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -970,7 +970,12 @@ Annotations are characters 128-255."
 
 (defun proof-font-lock-minor-mode ()
   "Start font-lock as a minor mode in the current buffer."
-  (and (fboundp 'font-lock-set-defaults) (font-lock-set-defaults)))
+
+  ;; setting font-lock-defaults explicitly is required by FSF Emacs
+  ;; 20.2's version of font-lock
+  (make-local-variable 'font-lock-defaults)
+  (setq font-lock-defaults '(font-lock-keywords))
+  (font-lock-set-defaults))
 
 (defun proof-goals-config-done ()
   "Initialise the goals buffer after the child has been configured."
diff --git a/generic/proof.el b/generic/proof.el
index 4239e250..7247e7c6 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -30,12 +30,6 @@
 (require 'cl)				
 
 
-;; FIXME da: I think these should all be autoloaded!!
-;; (require 'compile)
-;; (require 'comint)
-;; (require 'etags)			
-;; (require 'easymenu)
-
 ;; browse-url function doesn't seem to be autoloaded in
 ;; XEmacs 20.4, but it is in FSF Emacs 20.2.
 (or (fboundp 'browse-url)
@@ -145,7 +139,7 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
       (setq start (goto-char (point-max)))
       (insert str) (setq end (point))
       (newline)
-      ;; FIXME tms: Make this work for FSF Emacs 20.2
+      (font-lock-set-defaults)		;required for FSF Emacs 20.2
       (font-lock-fontify-region start end)
       (font-lock-append-text-property start end 'face face)
       (buffer-substring start end))))
diff --git a/isa/isa.el b/isa/isa.el
index cbc24ca4..a6aecd58 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -75,7 +75,7 @@ no regular or easily discernable structure."
 
 ;;; FIXME: test and add more things here
 (defcustom isa-outline-regexp
-  (ids-to-regexp '("goal" "Goal" "prove_goal"))
+  (proof-ids-to-regexp '("goal" "Goal" "prove_goal"))
   "Outline regexp for Isabelle ML files"
   :type 'regexp
   :group 'isabelle-config)
@@ -111,7 +111,7 @@ no regular or easily discernable structure."
    proof-save-command-regexp    isa-save-command-regexp
    proof-save-with-hole-regexp  isa-save-with-hole-regexp
    proof-goal-with-hole-regexp  isa-goal-with-hole-regexp
-   proof-commands-regexp	(ids-to-regexp isa-keywords)
+   proof-commands-regexp	(proof-ids-to-regexp isa-keywords)
    ;; proof engine commands (first three for menus, last for undo)
    proof-prf-string		"pr();"
    proof-goal-command		"Goal \"%s\";"
@@ -353,7 +353,7 @@ Resulting output from Isabelle will be parsed by Proof General."
 ;; FIXME: think about the next variable.  I've changed sense from
 ;;  LEGO and Coq's treatment.
 (defcustom isa-not-undoable-commands-regexp
-  (ids-to-regexp '("undo" "back"))
+  (proof-ids-to-regexp '("undo" "back"))
   "Regular expression matching commands which are *not* undoable."
   :type 'regexp
   :group 'isabelle-config)
diff --git a/lego/lego.el b/lego/lego.el
index a1c5b234..72b81f0b 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -11,6 +11,8 @@
 
 (require 'proof)
 (require 'proof-script)
+
+;;FIXME: proof-shell should be autoloaded
 (require 'proof-shell)
 (require 'lego-syntax)
 
diff --git a/todo b/todo
index 83a19f08..de9fab22 100644
--- a/todo
+++ b/todo
@@ -382,7 +382,8 @@ 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)
+C derive a coq-response-mode from proof-response-mode; see lego.el (10min)
+
 
 D set proof-commands-regexp to support indentation for commands
 						    (10min)
@@ -416,6 +417,8 @@ A* Check all regexps are suitable instantiated.
 
 A Fixup multiple file handling with theory loader hacks to Isabelle.
 
+C derive an isa-response-mode from proof-response-mode; see lego.el (10min) 
+
 D Implement completion for Isabelle using tables generated by
   the running process.