Many compatibility updates, bug fixes, rearrangements for compilation.

6 files changed, 89 insertions, 190 deletions

diff --git a/lib/bufhist.el b/lib/bufhist.el
index aa58a37d..4917819f 100644
--- a/lib/bufhist.el
+++ b/lib/bufhist.el
@@ -73,14 +73,18 @@
        indicator
        'help-echo desc
        'keymap (eval-when-compile
-		 (let ((map (make-sparse-keymap)))
-		   ;; FIXME: clicking can go wrong here because the
-		   ;; current buffer can be something else which has no hist!
-		   (define-key map [mode-line mouse-1] 'bufhist-prev)
-		   (define-key map [mode-line mouse-3] 'bufhist-next)
-;		   (define-key map [mode-line control mouse-1] 'bufhist-first)
-;		   (define-key map [mode-line control mouse-3] 'bufhist-last)
-		   map))
+		 (cond 
+		  ((featurep 'xemacs)
+		   nil)
+		  (t
+		   (let ((map (make-sparse-keymap)))
+		     ;; FIXME: clicking can go wrong here because the
+		     ;; current buffer can be something else which has no hist!
+		     (define-key map [mode-line mouse-1] 'bufhist-prev)
+		     (define-key map [mode-line mouse-3] 'bufhist-next)
+		     ;; (define-key map [mode-line control mouse-1] 'bufhist-first)
+		     ;; (define-key map [mode-line control mouse-3] 'bufhist-last)
+		   map))))
        'mouse-face 'mode-line-highlight))))
      
 ;simple:
diff --git a/lib/holes.el b/lib/holes.el
index a4db4a23..fa7f6f92 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -143,7 +143,7 @@ is), which is annoying.
 (defvar holes-default-hole (make-detached-span)
   "An empty detached hole used as the default hole.
 You should not use this variable.")
-(detach-span holes-default-hole)
+(span-detach holes-default-hole)
 (defvar holes-active-hole holes-default-hole
   "The current active hole.
 There can be only one active hole at a time,
@@ -366,7 +366,7 @@ Error if HOLE is not a hole."
 
 (defun holes-make-hole (start end)
   "Make and return an (span) hole from START to END."
-  (let ((ext (make-span start end)))
+  (let ((ext (span-make start end)))
     (set-span-properties
      ext `(
 	   hole t
@@ -419,7 +419,7 @@ the span."
   (if (and (holes-active-hole-exist-p) (eq holes-active-hole HOLE))
       (holes-disable-active-hole)
     )
-  (delete-span HOLE)
+  (span-delete HOLE)
   )
 
 (defun holes-clear-hole-at (&optional pos)
@@ -442,7 +442,7 @@ the span."
 (defun holes-mapcar-holes (FUNCTION &optional FROM TO PROP)
 					; checkdoc-params: (FUNCTION FROM TO PROP)
   "Internal."
-  (mapcar-spans FUNCTION FROM TO 'hole)
+  (span-mapcar-spans FUNCTION FROM TO 'hole)
   )
 
 (defun holes-clear-all-buffer-holes (&optional start end)
@@ -524,7 +524,7 @@ goal(FIXME?).  Use `replace-active-hole' instead."
 			     (or str (car kill-ring)) ;kill ring?
 			     (span-buffer exthole)
 			     )
-      (detach-span exthole) ;; this seems necessary for span overlays,
+      (span-detach exthole) ;; this seems necessary for span overlays,
       ;; where the buffer attached to the span is
       ;; not removed automatically by the fact
       ;; that the span is removed from the buffer
@@ -648,7 +648,7 @@ Sets `holes-active-hole' to the next hole if it exists."
 	       (eq sp holes-active-hole))
 	  (holes-disable-active-hole))
       (holes-replace "" sp)
-      (detach-span sp)
+      (span-detach sp)
       )
     (message "hole killed")
     )
@@ -678,7 +678,7 @@ Sets `holes-active-hole' to the next hole if it exists."
     (let ((ext (holes-hole-at-event event)))
       (if (eq ext holes-active-hole)
 	  (holes-disable-active-hole))
-      (detach-span ext)
+      (span-detach ext)
       )
     )
   (message "hole deleted")
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index 96a73ff3..43e8a2f2 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -10,27 +10,22 @@
 ;; operating systems and Emacs versions.  This is to help keep
 ;; track of them.
 ;;
-;; The development policy for Proof General is for the main codebase
-;; to be written for the latest stable version of GNU Emacs (previously
-;; XEmacs, not yet reworked since 3.7). 
-;; We follow GNU Emacs advice on removing obsolete function calls.
+;; The development policy for Proof General (since v3.7) is for the
+;; main codebase to be written for the latest stable version of GNU
+;; Emacs, following GNU Emacs advice on obsolete function calls.
 ;;
 
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
 ;;; Architecture flags
 ;;;
 
-(eval-and-compile
-(defvar proof-running-on-XEmacs (string-match "XEmacs" emacs-version)
-  "Non-nil if Proof General is running on XEmacs.")
-(defvar proof-running-on-Emacs21 (and (not proof-running-on-XEmacs)
-				      (>= emacs-major-version 21))
-  "Non-nil if Proof General is running on GNU Emacs 21 or later.")
-;; rough test for XEmacs on win32, anyone know about GNU Emacs on win32?
-(defvar proof-running-on-win32 (fboundp 'win32-long-file-name)
-  "Non-nil if Proof General is running on a win32 system.")
-)
+;; can use eval-and-compile to allow optimisation, but that would
+;; require recompilation for Windows
+(defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin))
+  "Non-nil if Proof General is running on a windows variant system.")
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -83,9 +78,7 @@ Search for COMMAND in exec-path and return the absolute file name.
 Return nil if COMMAND is not found anywhere in `exec-path'." nil nil))
 
 
-;; Compatibility with XEmacs 20.3/4
-(or (boundp 'path-separator)
-    (setq path-separator (if proof-running-on-win32 ";" ":")))
+;; Compatibility with XEmacs 20.3
 (or (fboundp 'split-path)
     (defun split-path (path)
       "Explode a search path into a list of strings.
@@ -95,50 +88,6 @@ with `path-separator'."
 
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;;
-;;; Window systems
-;;;
-
-;; A useful function of GNU Emacs: support it in XEmacs if not already there
-;; NOTE!  Unfortunately this is present in some XEmacs versions but
-;; returns the wrong value (e.g. nil on a graphic display).
-; (or (fboundp 'display-graphic-p)
-;     (defun display-graphic-p ()
-;       "Return non-nil if DISPLAY is a graphic display.
-; Graphical displays are those which are capable of displaying several
-; frames and several different fonts at once.  This is true for displays
-; that use a window system such as X, and false for text-only terminals."
-;       (not (memq (console-type) '(tty stream dead)))))
-
-;; Let's define our own version based on window-system.  
-;; Even though this is deprecated on XEmacs, it seems more likely
-;; that things will go wrong on badly ported Emacs than users
-;; using multiple devices, some of which are ttys...
-(defun pg-window-system ()
-  "Return non-nil if we're on a window system.  Simply use `window-system'."
-  (and window-system t))
-
-;; The next constant is used in proof-config for defface calls.
-;; Unfortunately defface uses window-system, which Emacs porters like
-;; to invent new symbols for each time, which is a pain.
-;; This list has the ones I know about so far.  
-
-(defconst pg-defface-window-systems 
-  '(x            ;; bog standard
-    mswindows    ;; Windows
-    gtk          ;; gtk emacs (obsolete?)
-    mac          ;; used by Aquamacs
-    carbon       ;; used by Carbon XEmacs
-    ns           ;; NeXTstep Emacs (Emacs.app)
-    x-toolkit)   ;; possible catch all (but probably not)
-  "A list of possible values for `window-system'.
-If you are on a window system and your value of `window-system' is
-not listed here, you may not get the correct syntax colouring behaviour.")
-
-
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -161,7 +110,8 @@ Unless optional argument INPLACE is non-nil, return a new string."
 
 ;; Required by xmltok.el [not used at present], proof-shell.el
 (or (fboundp 'replace-regexp-in-string)
-;; Code is taken from Emacs 21.1.1/subr.el 
+
+;; Code is taken from Emacs 21.1.1/subr.el. Now in XEmacs (21.5b28, at least)
 (defun replace-regexp-in-string (regexp rep string &optional
 					fixedcase literal subexp start)
   "Replace all matches for REGEXP with REP in STRING.
@@ -224,7 +174,7 @@ and replace a sub-expression, e.g.
 ;; :visible keyword.  To use that when it's available, we set a
 ;; constant to be :visible or :active
 
-(defconst menuvisiblep (if proof-running-on-Emacs21 :visible :active)
+(defconst menuvisiblep (if (featurep 'xemacs) :active :visible)
   ":visible (on GNU Emacs) or :active (otherwise). 
 The GNU Emacs implementation of easy-menu-define has a very handy
 :visible keyword.  To use that when it's available, we use this constant.")
@@ -294,7 +244,7 @@ The value returned is the value of the last form in BODY."
 ;; dynamic-completion-mode after loading it.
 (or (fboundp 'complete)
     (autoload 'complete "completion"))
-(unless proof-running-on-XEmacs
+(unless (featurep 'xemacs)
   (eval-after-load "completion"
     '(dynamic-completion-mode)))
 
@@ -317,64 +267,11 @@ The value returned is the value of the last form in BODY."
   "Dummy function for Proof General on GNU Emacs."
   (force-mode-line-update)))
 
-;; Interactive flag
-(or (fboundp 'noninteractive)
-    (defun noninteractive ()
-      "Dummy function for Proof General on GNU Emacs."
-      noninteractive))
-
-;; Replacing in string (useful function from subr.el in XEmacs 21.1.9)
+;; Replace in string: XEmacs original now in GNU Emacs as replace-regexp-in-string
 (or (fboundp 'replace-in-string)
-    (if (fboundp 'replace-regexp-in-string)
-      (defun replace-in-string (str regexp newtext &optional literal)
-        (replace-regexp-in-string regexp newtext str 'fixedcase literal))
-(defun replace-in-string (str regexp newtext &optional literal)
-  "Replace all matches in STR for REGEXP with NEWTEXT string,
- and returns the new string.
-Optional LITERAL non-nil means do a literal replacement.
-Otherwise treat \\ in NEWTEXT string as special:
-  \\& means substitute original matched text,
-  \\N means substitute match for \(...\) number N,
-  \\\\ means insert one \\."
-  ;; Not present in GNU
-  ;; (check-argument-type 'stringp str)
-  ;; (check-argument-type 'stringp newtext)
-  (let ((rtn-str "")
-	(start 0)
-	(special)
-	match prev-start)
-    (while (setq match (string-match regexp str start))
-      (setq prev-start start
-	    start (match-end 0)
-	    rtn-str
-	    (concat
-	      rtn-str
-	      (substring str prev-start match)
-	      (cond (literal newtext)
-		    (t (mapconcat
-			(lambda (c)
-			  (if special
-			      (progn
-				(setq special nil)
-				(cond ((eq c ?\\) "\\")
-				      ((eq c ?&)
-				       (substring str
-						  (match-beginning 0)
-						  (match-end 0)))
-				      ((and (>= c ?0) (<= c ?9))
-				       (if (> c (+ ?0 (length
-						       (match-data))))
-					   ;; Invalid match num
-					   (error "Invalid match num: %c" c)
-					 (setq c (- c ?0))
-					 (substring str
-						    (match-beginning c)
-						    (match-end c))))
-				      (t (char-to-string c))))
-			    (if (eq c ?\\) (progn (setq special t) nil)
-			      (char-to-string c))))
-			 newtext ""))))))
-    (concat rtn-str (substring str start))))))
+    (defun replace-in-string (str regexp newtext &optional literal)
+      (replace-regexp-in-string regexp newtext str 'fixedcase literal)))
+
 
 ;; An implemenation of buffer-syntactic-context for GNU Emacs
 (defun proof-buffer-syntactic-context-emulate (&optional buffer)
@@ -540,11 +437,11 @@ The value returned is the value of the last form in BODY."
 ;;; Attempt to harmonise pop-to-buffer behaviour 
 ;;;
 
-(if proof-running-on-Emacs21
+(or (featurep 'xemacs)
     ;; NB: GNU Emacs version has fewer args
     (defalias 'pg-pop-to-buffer 'pop-to-buffer))
 
-(if proof-running-on-XEmacs
+(if (featurep 'xemacs)
 ;; Version from XEmacs 21.4.12, with args to match GNU Emacs
 ;; NB: GNU Emacs version has fewer args, we don't use ON-FRAME
 (defun pg-pop-to-buffer (bufname &optional not-this-window-p no-record on-frame)
@@ -585,7 +482,7 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
       ;; select-window will modify the internal keyboard focus of XEmacs
       (select-window window))
     buf))
-);;; End XEmacs only
+)
 
   
 
@@ -630,7 +527,7 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
 ;; PG 3.5.1: add hack in proof-compat.el to deal with this
 (if
     (and
-     proof-running-on-Emacs21
+     (not (featurep 'xemacs))
      (or
       (string-equal emacs-version "21.2.1")
       (string-equal emacs-version "21.1.0")))
@@ -653,23 +550,23 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
 ;; in this function.  In XEmacs post 21.5 one can set names of buffers
 ;; to omit just from tabs list.
 
-(if proof-running-on-XEmacs
+(if (featurep 'xemacs)
     (progn
 
-(fset 'select-buffers-tab-buffers-by-mode-old 
-      (symbol-function 'select-buffers-tab-buffers-by-mode))
-
-(defun select-buffers-tab-buffers-by-mode (buf1 buf2)
-      (let* ((mode1 (symbol-value-in-buffer 'major-mode buf1)) ;; candidate buf
-	     (mode2 (symbol-value-in-buffer 'major-mode buf2)) ;; displayed buf
-	     (auxes '(proof-goals-mode proof-shell-mode proof-response-mode))
-	     (mode1aux (memq (get mode1 'derived-mode-parent) auxes))
-	     (mode2aux (memq (get mode2 'derived-mode-parent) auxes)))
-	(cond
-	 (mode1aux	mode2aux)
-	 (mode2aux	nil)
-	 (t             (select-buffers-tab-buffers-by-mode-old buf1 buf2)))))
-)) ;; end running-on-XEmacs
+      (fset 'select-buffers-tab-buffers-by-mode-old 
+	    (symbol-function 'select-buffers-tab-buffers-by-mode))
+
+      (defun select-buffers-tab-buffers-by-mode (buf1 buf2)
+	(let* ((mode1 (symbol-value-in-buffer 'major-mode buf1)) ;; candidate buf
+	       (mode2 (symbol-value-in-buffer 'major-mode buf2)) ;; displayed buf
+	       (auxes '(proof-goals-mode proof-shell-mode proof-response-mode))
+	       (mode1aux (memq (get mode1 'derived-mode-parent) auxes))
+	       (mode2aux (memq (get mode2 'derived-mode-parent) auxes)))
+	  (cond
+	   (mode1aux	mode2aux)
+	   (mode2aux	nil)
+	   (t             (select-buffers-tab-buffers-by-mode-old buf1 buf2)))))
+      )) ;; end XEmacs featurep
       
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -677,10 +574,10 @@ If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
 ;; Workaround GNU Emacs problems in easymenu-add
 ;;
 
-(if proof-running-on-Emacs21
-     ;; This has a nasty side effect of removing accelerators
-     ;; from existing menus when easy-menu-add is called.
-     ;; Problem confirmed in versions: 21.4.1, OK: 22.1.1
+(if (not (featurep 'xemacs))
+    ;; This has a nasty side effect of removing accelerators
+    ;; from existing menus when easy-menu-add is called.
+    ;; Problem confirmed in versions: 21.4.1, OK: 22.1.1
     (or (< emacs-major-version 22)
 	(setq easy-menu-precalculate-equivalent-keybindings nil)))
 
diff --git a/lib/span-extent.el b/lib/span-extent.el
index 78eb52f5..481933fc 100644
--- a/lib/span-extent.el
+++ b/lib/span-extent.el
@@ -9,29 +9,29 @@
 
 ;; XEmacs-Emacs compatibility: define "spans" in terms of extents.
 
-(defsubst make-span (start end)
+(defsubst span-make (start end)
   "Make a span for the range [START, END) in current buffer."
   (make-extent start end))
 
-(defsubst detach-span (span)
+(defsubst span-detach (span)
   "Remove SPAN from its buffer."
   (detach-extent span))
 
-(defsubst set-span-endpoints (span start end)
+(defsubst span-set-endpoints (span start end)
   "Set the endpoints of SPAN to START, END."
   (set-extent-endpoints span start end))
 
-(defsubst set-span-property (span name value)
+(defsubst span-set-property (span name value)
   "Set SPAN's property NAME to VALUE."
   (set-extent-property span name value))
 
 (defsubst span-read-only (span)
   "Set SPAN to be read only."
-  (set-span-property span 'read-only t))
+  (span-set-property span 'read-only t))
 
 (defsubst span-read-write (span)
   "Set SPAN to be writeable."
-  (set-span-property span 'read-only nil))
+  (span-set-property span 'read-only nil))
 
 (defun span-give-warning (&rest args)
   "Give a warning message."
@@ -40,19 +40,19 @@
 (defun span-write-warning (span)
   "Give a warning message when SPAN is changed."
   ;; FIXME: implement this in XEmacs, perhaps with after-change-functions
-  (set-span-property span 'read-only nil))
+  (span-set-property span 'read-only nil))
 
 (defsubst span-property (span name)
   "Return SPAN's value for property PROPERTY."
   (extent-property span name))
 
-(defsubst delete-span (span)
+(defsubst span-delete (span)
   "Delete SPAN."
   (let ((predelfn (span-property span 'span-delete-action)))
     (and predelfn (funcall predelfn)))
   (delete-extent span))
 
-(defsubst mapcar-spans (fn start end prop &optional val)
+(defsubst span-mapcar-spans (fn start end prop &optional val)
   "Apply function FN to all spans between START and END with property PROP set"
   (mapcar-extents fn nil (current-buffer) start end  nil prop val))
 
diff --git a/lib/span-overlay.el b/lib/span-overlay.el
index 1b4402db..1d246e87 100644
--- a/lib/span-overlay.el
+++ b/lib/span-overlay.el
@@ -11,11 +11,11 @@
 
 (defalias 'span-start 'overlay-start)
 (defalias 'span-end 'overlay-end)
-(defalias 'set-span-property 'overlay-put)
+(defalias 'span-set-property 'overlay-put)
 (defalias 'span-property 'overlay-get)
-(defalias 'make-span 'make-overlay)
-(defalias 'detach-span 'delete-overlay)
-(defalias 'set-span-endpoints 'move-overlay)
+(defalias 'span-make 'make-overlay)
+(defalias 'span-detach 'delete-overlay)
+(defalias 'span-set-endpoints 'move-overlay)
 (defalias 'span-buffer 'overlay-buffer)
 
 (defun span-read-only-hook (overlay after start end &optional len)
@@ -34,14 +34,14 @@
   ;; the buffer.  (Maybe read-only is only a text property, not an
   ;; overlay property?).
   ;; (overlay-put span 'read-only t))
-  (set-span-property span 'modification-hooks '(span-read-only-hook))
-  (set-span-property span 'insert-in-front-hooks '(span-read-only-hook)))
+  (span-set-property span 'modification-hooks '(span-read-only-hook))
+  (span-set-property span 'insert-in-front-hooks '(span-read-only-hook)))
 
 (defun span-read-write (span)
   "Set SPAN to be writeable."
   ;; See comment above for text properties problem.
-  (set-span-property span 'modification-hooks nil)
-  (set-span-property span 'insert-in-front-hooks nil))
+  (span-set-property span 'modification-hooks nil)
+  (span-set-property span 'insert-in-front-hooks nil))
 
 (defun span-give-warning (&rest args)
   "Give a warning message."
@@ -49,8 +49,8 @@
 
 (defun span-write-warning (span)
   "Give a warning message when SPAN is changed."
-  (set-span-property span 'modification-hooks '(span-give-warning))
-  (set-span-property span 'insert-in-front-hooks '(span-give-warning)))
+  (span-set-property span 'modification-hooks '(span-give-warning))
+  (span-set-property span 'insert-in-front-hooks '(span-give-warning)))
 
 ;; We use end first because proof-locked-queue is often changed, and
 ;; its starting point is always 1
@@ -79,14 +79,14 @@ For XEmacs, span-at gives smallest extent at pos.
 For Emacs, we assume that spans don't overlap."
   (car (spans-at-point-prop pt prop)))
 
-(defsubst delete-span (span)
+(defsubst span-delete (span)
   "Delete SPAN."
   (let ((predelfn (span-property span 'span-delete-action)))
     (and predelfn (funcall predelfn)))
   (delete-overlay span))
 
 ;; The next two change ordering of list of spans:
-(defsubst mapcar-spans (fn start end prop &optional val)
+(defsubst span-mapcar-spans (fn start end prop &optional val)
   "Apply function FN to all spans between START and END with property PROP set"
   (mapcar fn (spans-at-region-prop start end prop (or val nil))))
 
@@ -152,7 +152,7 @@ A span is before PT if it begins before the character before PT."
   "Set priority of span to make it appear above other spans.
 FIXME: new hack added nov 99 because of disappearing overlays.
 Behaviour is still worse than before."	;??? --Stef
-  (set-span-property span 'priority 100))
+  (span-set-property span 'priority 100))
 
 (defalias 'span-object 'overlay-buffer)
 
diff --git a/lib/span.el b/lib/span.el
index 8e2c05f4..6fd8371d 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -5,12 +5,10 @@
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
-
-;; FIXME: NAMESPACE!!!!!!!
-
 ;;
 ;; Spans are our abstraction of extents/overlays.
 ;;
+
 (eval-and-compile
   (cond ((string-match "XEmacs" emacs-version)  
 	 (require 'span-extent))
@@ -21,21 +19,21 @@
 ;; Generic functions built on low-level concrete ones.
 ;; 
 
-(defsubst delete-spans (start end prop)
+(defsubst span-delete-spans (start end prop)
   "Delete all spans between START and END with property PROP set."
-  (mapcar-spans 'delete-span start end prop))
+  (span-mapcar-spans 'span-delete start end prop))
 
 (defsubst span-property-safe (span name)
   "Like span-property, but return nil if SPAN is nil."
   (and span (span-property span name)))
   
-(defsubst set-span-start (span value)
+(defsubst span-set-start (span value)
   "Set the start point of SPAN to VALUE."
-  (set-span-endpoints span value (span-end span)))
+  (span-set-endpoints span value (span-end span)))
 
-(defsubst set-span-end (span value)
+(defsubst span-set-end (span value)
   "Set the end point of SPAN to VALUE."
-  (set-span-endpoints span (span-start span) value))
+  (span-set-endpoints span (span-start span) value))
 
 (provide 'span)
 ;; span.el ends here.