improved support for Info

  o employed `Info-default-directory-list' rather than
    `Info-directory-list' so that code also works for Emacs 19.34
  o setting of `Info-default-directory-list' now at proof level

3 files changed, 25 insertions, 12 deletions

diff --git a/coq.el b/coq.el
index 2ae1d55c..a94e00dc 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,12 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; Revision 1.25  1998/05/23 12:50:40  tms
+;; improved support for Info
+;;   o employed `Info-default-directory-list' rather than
+;;     `Info-directory-list' so that code also works for Emacs 19.34
+;;   o setting of `Info-default-directory-list' now at proof level
+;;
 ;; Revision 1.24  1998/05/22 11:31:33  hhg
 ;; Correct path for coq-prog-name and coq-tags.
 ;;
@@ -124,8 +130,6 @@
 (defvar coq-tags "/usr/local/lib/coq/theories/TAGS"
   "the default TAGS table for the Coq library")
 
-(defconst coq-info-dir "/usr/local/share/info")
-
 (defconst coq-process-config nil
   "Command to configure pretty printing of the Coq process for emacs.")
 
@@ -600,10 +604,6 @@
 		       ("coq"  . coq-tags))
 		     tag-table-alist)))
 
-;; Info
-  (if (not (memq coq-info-dir Info-directory-list))
-      (setq Info-directory-list	(cons coq-info-dir Info-directory-list)))
-
 ;; keymaps and menus
   (easy-menu-add coq-mode-menu coq-mode-map)
 
diff --git a/lego.el b/lego.el
index 74c1dbb6..cf7f128c 100644
--- a/lego.el
+++ b/lego.el
@@ -5,6 +5,12 @@
 
 
 ;; $Log$
+;; Revision 1.47  1998/05/23 12:50:42  tms
+;; improved support for Info
+;;   o employed `Info-default-directory-list' rather than
+;;     `Info-directory-list' so that code also works for Emacs 19.34
+;;   o setting of `Info-default-directory-list' now at proof level
+;;
 ;; Revision 1.46  1998/05/16 14:52:07  tms
 ;; implementation of `lego-shell-adjust-line-width' can now be called as
 ;; part of a hook. This change has been caused by replacing
@@ -125,8 +131,6 @@
 (defvar lego-tags "/home/tms/lib/lib_Type/TAGS"
   "the default TAGS table for the LEGO library")
 
-(defconst lego-info-dir "/usr/local/share/info")
-
 (defconst lego-process-config "Configure PrettyOn; Configure AnnotateOn;"
   "Command to enable pretty printing of the LEGO process.")
 
@@ -640,10 +644,6 @@
 
   (setq font-lock-keywords lego-font-lock-keywords-1)
 
-;; Info
-  (if (not (memq lego-info-dir Info-directory-list))
-      (setq Info-directory-list	(cons lego-info-dir Info-directory-list)))
-
 ;; where to find files
 
   (setq compilation-search-path (cons nil (lego-get-path)))
diff --git a/proof.el b/proof.el
index 734ecf31..f7d94ee5 100644
--- a/proof.el
+++ b/proof.el
@@ -9,6 +9,12 @@
 
 
 ;; $Log$
+;; Revision 1.46  1998/05/23 12:50:44  tms
+;; improved support for Info
+;;   o employed `Info-default-directory-list' rather than
+;;     `Info-directory-list' so that code also works for Emacs 19.34
+;;   o setting of `Info-default-directory-list' now at proof level
+;;
 ;; Revision 1.45  1998/05/22 09:46:58  tms
 ;; fixed a bug in proof-frob-locked-end
 ;;
@@ -244,6 +250,8 @@
 ;;               Configuration                                      ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(defconst proof-info-dir "/usr/local/share/info")
+
 (defvar proof-shell-cd nil
   "*Command of the inferior process to change the directory.") 
 
@@ -1768,6 +1776,11 @@ current command."
        (push (cons major-mode 'fume-match-find-next-function-name)
 	     fume-find-function-name-method-alist))
 
+;; Info
+  (or (memq proof-info-dir Info-default-directory-list)
+      (setq Info-default-directory-list
+	    (cons proof-info-dir Info-default-directory-list)))
+
 ;; keymap
 
   (define-key proof-mode-map [(meta tab)] 'tag-complete-symbol)