[nongnu] elpa/proof-general f6df849 2/2: Merge pull request #606 from ProofGeneral/dont-retract-on-indent

[ELPA Syncer]

branch: elpa/proof-general
commit f6df84995cf597a705df050e5abca4171d52db06
Merge: 38ae8fd b5052cd
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #606 from ProofGeneral/dont-retract-on-indent
    
    * generic/proof-script.el: Don't retract on indent (#604)
---
 coq/coq.el              |  6 ++----
 generic/pg-pbrpm.el     | 11 +++++------
 generic/proof-script.el | 18 +++++++++++++++---
 lib/span.el             |  7 +------
 4 files changed, 23 insertions(+), 19 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 84708c1..84ce891 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2732,10 +2732,8 @@ insertion point for the \"using\" annotation. ")
 
 (defun coq-insert-proof-using (_proof-pos _previous-content insert-point 
string-suggested)
   (goto-char insert-point)
-  (let ((spl proof-locked-span))
-    (span-read-write spl) ; temporarily make the locked span writable
-    (insert (concat " using " string-suggested))
-    (proof-span-read-only spl)))
+  (let ((proof--inhibit-retract-on-change t))
+    (insert (concat " using " string-suggested))))
 
 (defun coq-insert-suggested-dependency ()
   (interactive)
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 942cc91..2041800 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -1,4 +1,4 @@
-;; pg-pbrpm.el --- Proof General - Proof By Rules Pop-up Menu - mode.
+;; pg-pbrpm.el --- Proof General - Proof By Rules Pop-up Menu - mode.  -*- 
lexical-binding: t; -*-
 ;;
 ;; Copyright (C) 2004 - Universite de Savoie, France.
 ;; Authors:   Jean-Roch SOTTY, Christophe Raffalli
@@ -98,12 +98,10 @@ Matches the region to be returned.")
            (mapc (lambda (sp)
                    (let* ((p1 (span-start sp))
                           (p2 (span-end sp))
-                          (spl (span-at p1 'pglock)))
-                     (span-read-write spl)
+                          (proof--inhibit-retract-on-change t))
                      (goto-char p1)
                      (insert (span-string span))
-                     (delete-region (+ p1 len) (+ p2 len))
-                     (span-read-only spl)))
+                     (delete-region (+ p1 len) (+ p2 len))))
                  (span-property span 'occurrences)))))))
 
 
@@ -257,7 +255,8 @@ The prover command is processed via pg-pbrpm-run-command."
                       (insert-gui-button (make-gui-button
                                           (concat (int-to-string count) ")")
                                           'pg-pbrpm-run-command
-                                          (list command act spans)) pos))
+                                          (list command act spans))
+                                         pos))
                     (insert "\n")))
                 (insert-gui-button
                  (make-gui-button
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 639d51d..4855813 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2200,12 +2200,17 @@ be omitted from the vanilla action list obtained from 
SEMIS."
       (setq vanillas (proof-script-omit-proofs vanillas)))
     (proof-extend-queue lastpos vanillas)))
 
+(defvar proof--inhibit-retract-on-change nil)
+
 (defun proof-retract-before-change (beg end)
   "For `before-change-functions'.  Retract to BEG unless BEG and END in 
comment.
 No effect if prover is busy."
-  (when (and (> (proof-queue-or-locked-end) beg)
-            (not (and (proof-inside-comment beg)
-                      (proof-inside-comment end))))
+  (unless (or (<= (proof-queue-or-locked-end) beg)
+             proof--inhibit-retract-on-change
+             (and (proof-inside-comment beg)
+                  ;; FIXME: This may mis fire if a change starts in a comment
+                  ;; and ends in another but with non-comment code in-between.
+                  (proof-inside-comment end)))
     (when proof-shell-busy
       (message "Interrupting prover")
       (proof-interrupt-process)
@@ -2826,6 +2831,13 @@ finish setup which depends on specific proof assistant 
configuration."
       (proof-shell-make-associated-buffers)
       (proof-layout-windows))
 
+  ;; Allow reindenting the already-processed code without causing
+  ;; a retraction.
+  (add-function :around (local 'indent-line-function)
+                #'(lambda (orig-fun &rest args)
+                    (let ((proof--inhibit-retract-on-change t))
+                      (apply orig-fun args))))
+
   ;; Make sure the user has been welcomed!
   (proof-splash-message))
 
diff --git a/lib/span.el b/lib/span.el
index 48cfb3c..fccec29 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -51,11 +51,6 @@
   (span-set-property span 'modification-hooks '(span-read-only-hook))
   (span-set-property span 'insert-in-front-hooks '(span-read-only-hook)))
 
-(defun span-read-write (span)
-  "Set SPAN to be writeable."
-  (span-set-property span 'modification-hooks nil)
-  (span-set-property span 'insert-in-front-hooks nil))
-
 (defun span-write-warning (span fun)
   "Give a warning message when SPAN is changed, unless `inhibit-read-only' is 
non-nil."
   (let ((funs (list (lambda (_span afterp beg end &rest _)