diff options
| -rw-r--r-- | proof-dependencies-emacs19.el | 265 | ||||
| -rw-r--r-- | proof-dependencies-xemacs.el | 176 |
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) |