Dependencies of proof mode for xemacs

There may be one or two areas that can be unified with emacs19
dependencies.

1 files changed, 176 insertions, 0 deletions

diff --git a/proof-dependencies-xemacs.el b/proof-dependencies-xemacs.el
new file mode 100644
index 00000000..928b29ad
--- /dev/null
+++ b/proof-dependencies-xemacs.el
@@ -0,0 +1,176 @@
+; 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)