Don't mess with overlay priorities.

3 files changed, 14 insertions, 11 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 10e27da9..57319ca7 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -875,9 +875,9 @@ a popup with the information in it."
 	   (lambda (x)
 	     (save-excursion
 	       (let ((idspan (span-make s e)))
-	       (span-set-property idspan 'priority 90) ; highest
-	       (span-set-property idspan 'help-echo
-				  (pg-last-output-displayform))))))))))
+                 ;; (span-set-property idspan 'priority 90) ; highest
+                 (span-set-property idspan 'help-echo
+                                    (pg-last-output-displayform))))))))))
 
 (defvar proof-query-identifier-history nil
   "History for `proof-query-identifier'.")
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 535da59f..c55df53d 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -240,7 +240,7 @@ This is simply to display the dependency somehow."
       (let ((span (cadar nmspans)))
 	(proof-depends-save-old-face span)
 	(span-set-property span 'face 'proof-highlight-dependency-face)
-	(span-set-property span 'priority pg-dep-span-priority)
+	;; (span-set-property span 'priority pg-dep-span-priority)
 	(span-set-property span 'mouse-highlight nil)
 	(span-set-property span 'help-echo helpmsg))
       (setq nmspans (cdr nmspans)))))
@@ -251,7 +251,7 @@ This is simply to display the dependency somehow."
       (let ((span (cadar nmspans)))
 	(proof-depends-save-old-face span)
 	(span-set-property span 'face 'proof-highlight-dependent-face)
-	(span-set-property span 'priority pg-dep-span-priority)
+	;; (span-set-property span 'priority pg-dep-span-priority)
 	(span-set-property span 'mouse-highlight nil)
 	(span-set-property span 'help-echo helpmsg)
 	(span-set-property span 'balloon-help helpmsg))
@@ -277,7 +277,7 @@ This is simply to display the dependency somehow."
       (while span
 	(pg-set-span-helphighlights span 'nohighlight)
 	(proof-depends-restore-old-face span)
-	(span-set-property span 'priority pg-ordinary-span-priority)
+	;; (span-set-property span 'priority pg-ordinary-span-priority)
 	(setq span (next-span span 'type))))))
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index abbfefb3..fbd8c2b1 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -227,7 +227,8 @@ Also clear list of script portions."
   ;; Initialise queue span, remove it from buffer.
   (unless proof-queue-span
     (setq proof-queue-span (span-make 1 1))
-    (span-raise proof-queue-span))
+    ;; (span-raise proof-queue-span)
+    )
   (span-set-property proof-queue-span 'start-closed t)
   (span-set-property proof-queue-span 'end-open t)
   (proof-span-read-only proof-queue-span 'always)
@@ -236,7 +237,8 @@ Also clear list of script portions."
   ;; Initialise locked span, remove it from buffer
   (unless proof-locked-span
       (setq proof-locked-span (span-make 1 1))
-      (span-raise proof-locked-span))
+      ;; (span-raise proof-locked-span)
+      )
   (span-set-property proof-locked-span 'start-closed t)
   (span-set-property proof-locked-span 'end-open t)
   (proof-span-read-only proof-locked-span)
@@ -653,7 +655,7 @@ IDIOMSYM is a symbol and ID is a strings."
     (span-set-property controlspan 'children
 		       (cons span (span-property controlspan 'children)))
     (pg-set-span-helphighlights span proof-region-mouse-highlight-face)
-    (span-set-property span 'priority 10)  ; lower than default
+    ;; (span-set-property span 'priority 10) ; lower than default
     (if proof-disappearing-proofs
 	(pg-make-element-invisible 'proof proofid))))
 
@@ -729,7 +731,7 @@ also as the 'response property on the span.
 
 Optional argument MOUSEFACE means use the given face as a mouse highlight
 face, if it is a face, otherwise, if it is non-nil but not a face,
-do not add a mouse highlight.  
+do not add a mouse highlight.
 
 In any case, a mouse highlight and tooltip are only set if
 `proof-output-tooltips' is non-nil.
@@ -775,7 +777,8 @@ Argument FACE means add 'face property FACE to the span."
 	  (span-set-property newspan 'mouse-face mouseface)))
     (if face
 	(span-set-property newspan 'face face))
-    (span-set-property newspan 'priority 50)))
+    ;; (span-set-property newspan 'priority 50)
+    ))