Fixes for FSF overlay obscurity.

3 files changed, 18 insertions, 3 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 558901c1..2699dbac 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -154,7 +154,10 @@ Allocate spans if need be.  The spans are detached from the
 buffer, so the regions are made empty by this function."
   ;; Initialise queue span, remove it from buffer.
   (unless proof-queue-span
-      (setq proof-queue-span (make-span 1 1)))
+      (setq proof-queue-span (make-span 1 1))
+      ;; FIXME: span-raise is an FSF hack to make locked span appear.
+      ;; overlays still don't work as well as they did/should.
+      (span-raise proof-queue-span))
   (set-span-property proof-queue-span 'start-closed t)
   (set-span-property proof-queue-span 'end-open t)
   (proof-span-read-only proof-queue-span)
@@ -162,7 +165,8 @@ buffer, so the regions are made empty by this function."
   (detach-span proof-queue-span)
   ;; Initialise locked span, remove it from buffer
   (unless proof-locked-span
-      (setq proof-locked-span (make-span 1 1)))
+      (setq proof-locked-span (make-span 1 1))
+      (span-raise proof-locked-span))
   (set-span-property proof-locked-span 'start-closed t)
   (set-span-property proof-locked-span 'end-open t)
   (proof-span-read-only proof-locked-span)
@@ -1652,7 +1656,8 @@ command."
 ;; User-level functions.
 ;;
 ;; FIXME: put these in a new file, proof-user, which defines
-;; user-level scripting mode.
+;; user-level scripting mode.  Or put stuff above in a new
+;; file, proof-core.el for low-level scripting functions.
 ;;
 
 
diff --git a/generic/span-extent.el b/generic/span-extent.el
index 0efca6c1..d54c0723 100644
--- a/generic/span-extent.el
+++ b/generic/span-extent.el
@@ -97,4 +97,8 @@ A span is before PT if it covers the character before PT."
        (extent-live-p span)
        (buffer-live-p (extent-object span))))
 
+(defun span-raise (span)
+  "Function added for FSF Emacs compatibility.  Do nothing here."
+  nil)
+
 (provide 'span-extent)
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index 87a57da2..cfc93020 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -280,4 +280,10 @@ If there are two spans overlapping then this won't work."
        (overlay-buffer span)
        (buffer-live-p (overlay-buffer span))))
 
+(defun span-raise (span)
+  "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."
+  (set-span-property span 'priority 100))
+
 (provide 'span-overlay)