improved help submenu for LEGO

  - added a link to the library and the reference card for version 1.3

3 files changed, 36 insertions, 41 deletions

diff --git a/lego.el b/lego.el
index 94969136..b8a398e1 100644
--- a/lego.el
+++ b/lego.el
@@ -25,6 +25,12 @@
   "*If non-nil, ask user for permission to save the current buffer before
   processing a module.")
 
+(defvar lego-help-menu-list
+  '(["The LEGO Reference Card" (w3-fetch lego-www-refcard) t]
+    ["The LEGO library (WWW)" (w3-fetch lego-library-www-page)  t])
+  "List of menu items, as defined in `easy-menu-define' for LEGO
+  specific help.")
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; Configuration of Generic Proof Package ;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -64,22 +70,17 @@
 
 (defvar lego-www-home-page "http://www.dcs.ed.ac.uk/home/lego/")
 
-(defvar lego-www-refcard (concat (w3-remove-file-name lego-www-home-page)
-				 "refcard.dvi.gz"))
-
-;; `lego-www-refcard' ought to be set to
-;; "ftp://ftp.dcs.ed.ac.uk/pub/lego/refcard.dvi.gz", but  
-;;    a) w3 fails to decode the image before invoking xdvi
-;;    b) ftp.dcs.ed.ac.uk is set up in a too non-standard way 
-
-
-(defvar lego-library-www-page
+(defvar lego-www-latest-release
   (concat (w3-remove-file-name lego-www-home-page)
-          "html/library/newlib.html"))
+  "html/release-1.3/")
+  "The WWW address for the latest LEGO release.")
+	  
+(defvar lego-www-refcard (concat lego-www-latest-release
+				 "refcard.ps.gz"))
 
-(defvar lego-www-customisation-page
-  (concat (w3-remove-file-name lego-www-home-page)
-          "html/emacs-customisation.html"))
+(defvar lego-library-www-page
+  (concat lego-www-latest-release "library/library.html")
+  "The HTML documentation of the LEGO library.")
 
 ;; ----- legostat and legogrep, courtesy of Mark Ruys
 
@@ -153,7 +154,9 @@
 
 (define-derived-mode lego-mode proof-mode
    "lego" "Lego Mode"
-   (lego-mode-config))
+   (lego-mode-config)
+   (easy-menu-change (list proof-mode-name) (car proof-help-menu)
+		     (append (cdr proof-help-menu) lego-help-menu-list)))
 
 (define-derived-mode lego-pbp-mode pbp-mode
   "pbp" "Proof-by-pointing support for LEGO"
diff --git a/proof.el b/proof.el
index 802078ae..2d3988e9 100644
--- a/proof.el
+++ b/proof.el
@@ -7,8 +7,6 @@
 ;;           James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens  
 
 
-
-
 (require 'cl)
 (require 'compile)
 (require 'comint)
@@ -45,7 +43,8 @@
 (defvar proof-shell-cd nil
   "*Command of the inferior process to change the directory.") 
 
-(defconst proof-info-dir "/usr/local/share/info")
+(defconst proof-info-dir "/usr/local/share/info"
+  "Directory to search for Info documents on Script Management.")
 
 (defvar proof-universal-keys
   (list (cons '[(control c) (control c)] 'proof-interrupt-process)
@@ -177,6 +176,8 @@
 ;;  Internal variables used by scripting and pbp                    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(defvar proof-mode-name "Proof")
+
 (defvar proof-shell-echo-input t
   "If nil, input to the proof shell will not be echoed")
 
@@ -1549,20 +1550,16 @@ deletes the region corresponding to the proof sequence."
   (interactive)
   (proof-restart-script))
 
-;;; The following was particular to LEGO:
-;;;	    ("Help"
-;;;	     ["The LEGO Reference Card" (w3-fetch lego-www-refcard) t]
-;;;	     ["The LEGO library (WWW)"
-;;;	      (w3-fetch lego-library-www-page)  t]
-;;;	     ["The LEGO Proof-assistant (WWW)"
-;;;	      (w3-fetch lego-www-home-page)  t]
-;;;	     ["Help on Emacs LEGO-mode" lego-info-mode  t]
-;;;	     ["Customisation" (w3-fetch lego-www-customisation-page)
-;;;	      t]
-;;;            ))))
+(defvar proof-help-menu
+  '("Help"
+	     ["Proof assistant web page"
+	      (w3-fetch proof-www-home-page) t]
+	     ["Help on Emacs proof-mode" proof-info-mode t]
+	     )
+  "The Help Menu in Script Management.")
 
 (defvar proof-shared-menu
-  (append '(
+  (append-element '(
             ["Display context" proof-ctxt
 	      :active (proof-shell-live-buffer)]
             ["Display proof state" proof-prf
@@ -1571,11 +1568,8 @@ deletes the region corresponding to the proof sequence."
 	      :active (proof-shell-live-buffer)]
 	    "----"
 	    ["Find definition/declaration" find-tag-other-window t]
-	    ("Help"
-	     ["Proof assistant web page"
-	      (w3-fetch proof-www-home-page) t]
-	     ["Help on Emacs proof-mode" proof-info-mode t]
-	     ))))
+	    )
+	  proof-help-menu))
 
 (defvar proof-menu  
   (append '("Commands"
@@ -1651,7 +1645,7 @@ current command."
 
 
 (define-derived-mode proof-mode fundamental-mode 
-  "Proof" "Proof mode - not standalone"
+  proof-mode-name "Proof mode - not standalone"
   ;; define-derived-mode proof-mode initialises proof-mode-map
   (setq proof-buffer-type 'script))
 
@@ -1671,12 +1665,12 @@ current command."
 (easy-menu-define proof-shell-menu
 		  proof-shell-mode-map
 		  "Menu used in the proof assistant shell."
-		  (cons "Proof" (cdr proof-shell-menu)))
+		  (cons proof-mode-name (cdr proof-shell-menu)))
 
 (easy-menu-define proof-mode-menu  
 		  proof-mode-map
 		  "Menu used in proof mode."
-		  (cons "Proof" (cdr proof-menu)))
+		  (cons proof-mode-name (cdr proof-menu)))
 
 ;; the following callback is an irritating hack - there should be some
 ;; elegant mechanism for computing constants after the child has
@@ -1790,7 +1784,7 @@ current command."
       (error "Failed to initialise proof process"))))
 
 (define-derived-mode pbp-mode fundamental-mode 
-  "Proof" "Proof by Pointing"
+  proof-mode-name "Proof by Pointing"
   ;; defined-derived-mode pbp-mode initialises pbp-mode-map
   (setq proof-buffer-type 'pbp)
   (suppress-keymap pbp-mode-map 'all)
diff --git a/todo b/todo
index 05ae2c3a..6600efc7 100644
--- a/todo
+++ b/todo
@@ -101,8 +101,6 @@ C pbp code doesn't quite accord with the tech report; in particular it
 
 A fix Pbp implementation (10h; tms)
 
-A Implement menu at generic level. (30min tms)
-
 A Sometimes e.g., ~tms/lego/imperative/recursion/Prepare_vc.l,
   annotations are recorded in the object file. This needs to be
   changed in the SML code. (initially 2h tms)