diff options
| -rw-r--r-- | generic/proof-site.el | 4 | ||||
| -rw-r--r-- | generic/proof.el | 25 | ||||
| -rw-r--r-- | lego/lego.el | 15 |
3 files changed, 24 insertions, 20 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 85a83007..97b4dc7e 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -102,9 +102,9 @@ You can use customize to set this variable." proof-internal-assistant-table) (concat "*Choice of proof assitants to use with Proof General. -A list of symbols chosen from: " +A list of symbols chosen from:" (apply 'concat (mapcar (lambda (astnt) - (concat "'" (symbol-name (car astnt)) " ")) + (concat " '" (symbol-name (car astnt)))) proof-internal-assistant-table)) ".\nEach proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General diff --git a/generic/proof.el b/generic/proof.el index 26cffe60..0965c400 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -198,7 +198,12 @@ No effect if proof-display-splash-time is zero." (require 'proof-syntax) (require 'proof-indent) -(autoload 'w3-fetch "w3" nil t) ; FIXME: shouldn't we use browse-url? + +;; browse-url function doesn't seem to be autoloaded in +;; XEmacs 20.4, is in FSF Emacs 20.2. +(or (fboundp 'browse-url) + (autoload 'browse-url "browse-url" + "Ask a WWW browser to load URL." t)) (defmacro deflocal (var value &optional docstring) "Define a buffer local variable VAR with default value VALUE." @@ -231,6 +236,12 @@ No effect if proof-display-splash-time is zero." "*If non-nil, format for newlines after each proof command in a script." :type 'boolean :group 'proof) + +(defcustom proof-general-home-page + "http://www.dcs.ed.ac.uk/home/proofgen" + "*Web address for Proof General" + :type 'string + :group 'proof-internal) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -2593,11 +2604,13 @@ Start up the proof assistant if necessary." (proof-restart-script)) (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] - ) + `("Help" + [,(concat proof-assistant " web page") + (browse-url proof-www-home-page) t] + ["Proof General home page" + (browse-url proof-general-home-page) t] + ["Proof General Info" proof-info-mode t] + ) "The Help Menu in Script Management.") (defvar proof-shared-menu diff --git a/lego/lego.el b/lego/lego.el index 94d5f82c..a35d28bf 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -35,8 +35,8 @@ :group 'lego) (defcustom 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]) + '(["The LEGO Reference Card" (browse-url lego-www-refcard) t] + ["The LEGO library (WWW)" (browse-url lego-library-www-page) t]) "List of menu items, as defined in `easy-menu-define' for LEGO specific help." :type '(repeat sexp) @@ -82,17 +82,8 @@ :type 'string :group 'lego) -;; FIXME da: this doesn't belong here, it's only used by lego. -;; (and it shouldn't be called w3-* !!) -(defun w3-remove-file-name (address) - "Remove the file name in a World Wide Web address" - (string-match "://[^/]+/" address) - (concat (substring address 0 (match-end 0)) - (file-name-directory (substring address (match-end 0))))) - (defcustom lego-www-latest-release - (concat (w3-remove-file-name lego-www-home-page) - "html/release-1.3/") + "http://www.dcs.ed.ac.uk/home/lego/html/release-1.3/" "The WWW address for the latest LEGO release." :type 'string :group 'lego) |