Dependencies on versions of emacs have been moved to span-extent.el

and span-overlay.el.

2 files changed, 0 insertions, 441 deletions

diff --git a/proof-dependencies-emacs19.el b/proof-dependencies-emacs19.el
deleted file mode 100644
index 487265a5..00000000
--- a/proof-dependencies-emacs19.el
+++ /dev/null
@@ -1,265 +0,0 @@
-; This file is an attempt to abstract away from the differences between
-; XEmacs and FSF Emacs. Everything that is done differently between one
-; or other version should be appropriately wrapped in here.
-
-; This is currently under development for emacs19.
-
-(defvar proof-locked-hwm nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-loose-end nil
-  "Limit of the queue region that is not equal to proof-locked-hwm.")
-
-(defvar last-span nil
-  "Start of backwards-linked list of spans")
-
-;; We build lists of spans both in the pbp buffer and in the scripting
-;; buffer.
-(make-variable-buffer-local 'last-span)
-
-
-(defsubst span-start (span)
-  (overlay-start span))
-
-(defsubst span-end (span)
-  (overlay-end span))
-
-(defun add-span (span l)
-  (cond (l (if (< (span-start span) (span-start l))
-	       (progn
-		 (overlay-put l 'before
-			      (add-span span (overlay-get l 'before)))
-		 l)
-	     (overlay-put span 'before l)
-	     span))
-	(t span)))
-
-(defsubst make-span (start end)
-  (setq last-span (add-span (make-overlay start end) last-span)))
-
-(defsubst set-span-endpoints (span start end)
-  (move-overlay span start end))
-
-(defsubst set-span-start (span value)
-  (overlay-start span value))
-
-(defsubst set-span-end (span value)
-  (overlay-end span value))
-
-(defsubst span-property (span name)
-  (overlay-get span name))
-
-(defsubst set-span-property (span name value)
-  (overlay-put span name value))
-
-;; relies on only being called from delete-span, and so resets value
-;; of last-span
-(defun remove-span (span l)
-  (cond ((not l) ())
-	((eq span l) (setq last-span (span-property l 'before)))
-	((eq span (span-property l 'before))
-	 (set-span-property l 'before (span-property span 'before))
-	 l)
-	(t (remove-span span (span-property l 'before)))))
-
-(defsubst delete-span (span)
-  (remove-span span last-span)
-  (delete-overlay span))
-
-(defun spans-at (start end)
-  (let ((overlays nil) (pos start) (os nil))
-    (while (< pos end)
-      (setq os (overlays-at pos))
-      (while os
-	(if (not (memq (car os) overlays))
-	    (setq overlays (cons (car os) overlays)))
-	(setq os (cdr os)))
-      (setq pos (next-overlay-change pos)))
-    overlays))
-
-(defun spans-at-prop (start end prop)
-  (let ((f (cond
-	    (prop (lambda (spans span)
-		    (if (span-property span prop) (cons span spans)
-		      spans)))
-	    (t (lambda (spans span) (cons span spans))))))
-    (foldl f nil (spans-at start end))))
-
-(defun type-prop (spans span)
-  (if (span-property span 'type) (cons span spans) spans))
-
-(defun spans-at-type (start end)
-  (foldl 'type-prop nil (spans-at start end)))
-
-(defsubst delete-spans (start end prop)
-  (mapcar 'delete-span (spans-at-prop start end prop)))
-
-(defun map-spans-aux (f l)
-  (cond (l (cons (funcall f l) (map-spans-aux f (span-property l 'before))))
-	(t ())))
-
-(defsubst map-spans (f)
-  (map-spans-aux f last-span))
-
-;; extent-at gives "smallest" extent at pos
-;; we're assuming right now that spans don't overlap
-(defun span-at (pt prop)
-  (car (spans-at-prop pt (+ pt 1) prop)))
-
-(defun find-span-aux (prop-p l)
-  (cond ((not l) ())
-	((funcall prop-p l) l)
-	(t (find-span-aux prop-p (span-property l 'before)))))
-
-(defun find-span (prop-p)
-  (find-span-aux prop-p last-span))
-
-(defun span-at-before (pt prop)
-  (let ((prop-pt-p
-	 (cond (prop (lambda (span)
-		       (and (> pt (span-start span))
-			    (span-property span prop))))
-	       (t (lambda (span) (> pt (span-end span)))))))
-    (find-span prop-pt-p)))
-  
-(defun prev-span (span prop)
-  (let ((prev-prop-p
-	 (cond (prop (lambda (span) (span-property span prop)))
-	       (t (lambda (span) t)))))
-    (find-span-aux prev-prop-p (span-property span 'before))))
-
-(defun next-span-aux (prop spans)
-  (cond ((not spans) nil)
-	((span-property (car spans) prop) (car spans))
-	(t (next-span-aux prop (cdr spans)))))
-
-;; overlays are [start, end)
-(defun next-span (span prop)
-  (next-span-aux prop
-		 (overlays-at (next-overlay-change (overlay-start span)))))
-
-(defvar proof-locked-span nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-span nil
-  "Upper limit of the locked region")
-
-(defun proof-init-segmentation ()
-  (setq proof-queue-loose-end nil)
-  (setq proof-queue-span (make-span 0 0))
-  (set-span-property proof-queue-span 'start-closed t)
-  (set-span-property proof-queue-span 'end-open t)
-  (set-span-property proof-queue-span 'read-only t)
-  (make-face 'proof-queue-face)
-
-;; Whether display has color or not
-  (cond (running-xemacs
-	 (if (eq (device-class (frame-device)) 'color)
-	     (set-face-background 'proof-queue-face "mistyrose")))
-	(running-emacs19
-	 (if (and window-system (x-display-color-p))
-	     (set-face-background 'proof-queue-face "mistyrose")))
-        (t (progn
-	     (set-face-background 'proof-queue-face "Black")
-	     (set-face-foreground 'proof-queue-face "White"))))
-
-  (set-span-property proof-queue-span 'face 'proof-queue-face)
-  
-  (setq proof-locked-hwm nil)
-  (setq proof-locked-span (make-span 0 0))
-  (set-span-property proof-locked-span 'start-closed t)
-  (set-span-property proof-locked-span 'end-open t)
-  (set-span-property proof-locked-span 'read-only t)
-;; don't know how to know if it has color or not
-;; Whether display has color or not
-  (cond (running-xemacs
-	 (if (eq (device-class (frame-device)) 'color)
-	     (progn (make-face 'proof-locked-face)
-		    (set-face-background 'proof-locked-face "lavender")
-		    (set-span-property proof-locked-span 'face
-				       'proof-locked-face))))
-	(running-emacs19
-	 (if (and window-system (x-display-color-p))
-	     (progn (make-face 'proof-locked-face)
-		    (set-face-background 'proof-locked-face "lavender")
-		    (set-span-property proof-locked-span 'face
-				       'proof-locked-face))))
-        (t (set-span-property proof-locked-span 'face 'underline))))
-
-;; for read-only, not done:
-(defsubst proof-lock-unlocked ()
-;;  (set-span-property proof-locked-span 'read-only t)
-  ())
-
-;; for read-only, not done:
-(defsubst proof-unlock-locked ()
-;;  (set-span-property proof-locked-span 'read-only nil)
-  ())
-
-(defsubst proof-set-queue-endpoints (start end)
-  (set-span-endpoints proof-queue-span start end))
-
-(defsubst proof-detach-queue ()
-  (if proof-queue-span
-      (proof-set-queue-endpoints 0 0)))
-
-(defsubst proof-set-queue-start (start)
-  (set-span-endpoints proof-queue-span start (span-end proof-queue-span)))
-
-(defsubst proof-set-queue-end (end)
-  (set-span-endpoints proof-queue-span (span-start proof-queue-span) end))
-
-(defun proof-detach-segments ()
-  (if proof-queue-span
-      (set-span-endpoints proof-queue-span 0 0))
-  (if proof-locked-span
-      (set-span-endpoints proof-locked-span 0 0)))
-
-(defsubst proof-set-locked-end (end)
-  (set-span-endpoints proof-locked-span (point-min) end))
-
-(defsubst proof-locked-end ()
-  (or (and proof-locked-span (span-end proof-locked-span))
-      (point-min)))
-
-(defsubst proof-end-of-queue ()
-  (span-end proof-queue-span))
-
-(defun proof-dont-show-annotations ()
-  (let ((disp (make-display-table))
-	(i 128))
-	(while (< i 256)
-;; This is different from xemacs:
-	  (aset disp i [])
-	  (incf i))
-;; I believe the following sets display table of current buffer:
-	(setq buffer-display-table disp)))
-
-;; in case Emacs is not aware of read-shell-command-map
-(defvar read-shell-command-map
-  (let ((map (make-sparse-keymap)))
-    (if (not (fboundp 'set-keymap-parents))
-        (setq map (append minibuffer-local-map map))
-      (set-keymap-parents map minibuffer-local-map)
-      (set-keymap-name map 'read-shell-command-map))
-    (define-key map "\t" 'comint-dynamic-complete)
-    (define-key map "\M-\t" 'comint-dynamic-complete)
-    (define-key map "\M-?" 'comint-dynamic-list-completions)
-    map)
-  "Minibuffer keymap used by shell-command and related commands.")
-
-
-;; in case Emacs is not aware of the function read-shell-command
-(or (fboundp 'read-shell-command)
-    ;; from minibuf.el distributed with XEmacs 19.11
-    (defun read-shell-command (prompt &optional initial-input history)
-      "Just like read-string, but uses read-shell-command-map:
-\\{read-shell-command-map}"
-      (let ((minibuffer-completion-table nil))
-        (read-from-minibuffer prompt initial-input read-shell-command-map
-                              nil (or history
-                              'shell-command-history)))))
-
-
-
-(provide 'proof-dependencies-emacs19)
diff --git a/proof-dependencies-xemacs.el b/proof-dependencies-xemacs.el
deleted file mode 100644
index 928b29ad..00000000
--- a/proof-dependencies-xemacs.el
+++ /dev/null
@@ -1,176 +0,0 @@
-; This file is an attempt to abstract away from the differences between
-; XEmacs and FSF Emacs. Everything that is done differently between one
-; or other version should be appropriately wrapped in here.
-
-;; The package fume-func provides a function with the same name and
-;; specification. However, fume-func's version is incorrect.
-(defun fume-match-find-next-function-name (buffer)
-  "General next function name in BUFFER finder using match.
-  The regexp is assumed to be a two item list the car of which is the regexp
-  to use, and the cdr of which is the match position of the function name"
-  (set-buffer buffer)
-  (let ((r (car fume-function-name-regexp))
-        (p (cdr fume-function-name-regexp)))
-    (and (re-search-forward r nil t)
-	 (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))
-
-;; Now define "spans", which are intended to unify xemacs and emacs19
-(defvar proof-locked-hwm nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-loose-end nil
-  "Limit of the queue region that is not equal to proof-locked-hwm.")
-
-
-(defsubst make-span (start end)
-  (make-extent start end))
-
-(defsubst set-span-endpoints (span start end)
-  (set-extent-endpoints span start end))
-
-(defsubst set-span-start (span value)
-  (set-extent-endpoints span value (extent-end-position span)))
-
-(defsubst set-span-end (span value)
-  (set-extent-endpoints span (extent-start-position span) value))
-
-(defsubst span-property (span name)
-  (extent-property span name))
-
-(defsubst set-span-property (span name value)
-  (set-extent-property span name value))
-
-(defsubst delete-span (span)
-  (delete-extent span))
-
-(defsubst delete-spans (start end prop)
-  (mapcar-extents 'delete-extent nil (current-buffer) start end  nil prop))
-
-(defsubst span-at (pt prop)
-  (extent-at pt nil prop))
-
-(defsubst span-at-before (pt prop)
-  (extent-at pt nil prop nil 'before))
-  
-(defsubst span-start (span)
-  (extent-start-position span))
-
-(defsubst span-end (span)
-  (extent-end-position span))
-
-(defsubst prev-span (span prop)
-  (extent-at (extent-start-position span) nil prop nil 'before))
-
-(defsubst next-span (span prop)
-  (extent-at (extent-end-position span) nil prop nil 'after))
-
-(defvar proof-locked-ext nil
-  "Upper limit of the locked region")
-
-(defvar proof-queue-ext nil
-  "Upper limit of the locked region")
-
-(defun proof-init-segmentation ()
-  (setq proof-queue-loose-end nil)
-  (setq proof-queue-ext (make-extent nil nil (current-buffer)))
-  (set-extent-property proof-queue-ext 'start-closed t)
-  (set-extent-property proof-queue-ext 'end-open t)
-  (set-extent-property proof-queue-ext 'read-only t)
-  (make-face 'proof-queue-face)
-  (if (eq (device-class (frame-device)) 'color)
-	     (set-face-background 'proof-queue-face "mistyrose")
-    (set-face-background 'proof-queue-face "Black")
-    (set-face-foreground 'proof-queue-face "White"))
-  (set-extent-property proof-queue-ext 'face 'proof-queue-face)
-  
-  (setq proof-locked-hwm nil)
-  (setq proof-locked-ext (make-extent nil nil (current-buffer)))
-  (set-extent-property proof-locked-ext 'start-closed t)
-  (set-extent-property proof-locked-ext 'end-open t)
-  (set-extent-property proof-locked-ext 'read-only t)
-  (if (eq (device-class (frame-device)) 'color)
-      (progn (make-face 'proof-locked-face)
-	     (set-face-background 'proof-locked-face "lavender")
-	     (set-extent-property proof-locked-ext 'face 'proof-locked-face))
-    (set-extent-property proof-locked-ext 'face 'underline)))
-
-(defsubst proof-lock-unlocked ()
-  (set-extent-property proof-locked-ext 'read-only t))
-
-(defsubst proof-unlock-locked ()
-  (set-extent-property proof-locked-ext 'read-only nil))
-
-(defsubst proof-detach-queue ()
-  (if proof-queue-ext
-      (detach-extent proof-queue-ext)))
-
-(defsubst proof-detach-locked ()
-  (if proof-locked-ext
-      (detach-extent proof-locked-ext)))
-
-(defsubst proof-set-queue-endpoints (start end)
-  (set-extent-endpoints proof-queue-ext start end))
-
-(defsubst proof-set-queue-start (start)
-  (set-extent-endpoints proof-queue-ext start 
-			(extent-end-position proof-queue-ext)))
-
-(defsubst proof-set-queue-end (end)
-  (set-extent-endpoints proof-queue-ext (extent-start-position proof-queue-ext)
-			end)) 
-
-(defsubst proof-detach-segments ()
-  (proof-detach-queue)
-  (proof-detach-locked))
-
-(defsubst proof-set-locked-end (end)
-  (if (>= (point-min) end)
-      (proof-detach-locked)
-    (set-extent-endpoints proof-locked-ext (point-min) end)))
-
-(defsubst proof-locked-end ()
-  (or (and proof-locked-ext (extent-end-position proof-locked-ext))
-      (point-min)))
-
-(defsubst proof-end-of-queue ()
-  (extent-end-position proof-queue-ext))
-
-;(defsubst proof-have-color ()
-;  (eq (device-class) 'color))
-
-(defun proof-dont-show-annotations ()
-  (let ((disp (make-display-table))
-	(i 128))
-	(while (< i 256)
-	  (aset disp i "")
-	  (incf i))
-	(add-spec-to-specifier current-display-table disp (current-buffer))))
-
-;; in case Emacs is not aware of read-shell-command-map
-(defvar read-shell-command-map
-  (let ((map (make-sparse-keymap)))
-    (if (not (fboundp 'set-keymap-parents))
-        (setq map (append minibuffer-local-map map))
-      (set-keymap-parents map minibuffer-local-map)
-      (set-keymap-name map 'read-shell-command-map))
-    (define-key map "\t" 'comint-dynamic-complete)
-    (define-key map "\M-\t" 'comint-dynamic-complete)
-    (define-key map "\M-?" 'comint-dynamic-list-completions)
-    map)
-  "Minibuffer keymap used by shell-command and related commands.")
-
-
-;; in case Emacs is not aware of the function read-shell-command
-(or (fboundp 'read-shell-command)
-    ;; from minibuf.el distributed with XEmacs 19.11
-    (defun read-shell-command (prompt &optional initial-input history)
-      "Just like read-string, but uses read-shell-command-map:
-\\{read-shell-command-map}"
-      (let ((minibuffer-completion-table nil))
-        (read-from-minibuffer prompt initial-input read-shell-command-map
-                              nil (or history
-                              'shell-command-history)))))
-
-
-
-(provide 'proof-dependencies-xemacs)