Adding newline reverts processed block

[tchajed]

Whenever I add a newline after a processed region, it gets reverted. I'm using evil, which exacerbates this problem since I tend to use o to create newlines after the currently processed region fairly frequent. Proof General handles this correctly, which isn't very surprising since the sentence is unaffected.

This seems like an excellent feature for me to implement, but I wanted to record the feature request first.

[cpitclaudel]

Patches would indeed be lovely. Just to make sure I understand, though: can you give a concrete example?

[tchajed]

Sure. Create a file with just one line:

module Test

With the point at the end of the line, process the buffer (C-c C-RET), then create a newline (RET). Currently, this reverts everything. I'd like module Test to remain processed.

[cpitclaudel]

Thanks. But you wouldn't want it to stay processed if you had e.g.

module Test

let a = 1

and you added the line after module Test, right?

[tchajed]

No, even in that case, module Test can remain processed, unless I'm missing something and later parts of the file can affect earlier ones.

[cpitclaudel]

There's actually a bug in PG related to this, which we should be careful about: if you type this:

Module A.
  Module B.
  End B.
End A.

Module C := A.

… then you can add .B. to the end of that line, and PG won't revert. But if you then revert the whole file, things will go through just fine.

[cpitclaudel]

No, even in that case, module Test can remain processed, unless I'm missing something and later parts of the file can affect earlier ones.

Right — but it's ok for let a to be reverted, correct?

[tchajed]

Yes, that is expected.

[cpitclaudel]

Got it. What you're describing is the old behavior. I changed it because of the module issue above, but it should be easy to change it back. The relevant bit of code is this:

(defun fstar-subp-enqueue-until (end &optional no-error)
  "Mark region up to END busy, and enqueue the newly created overlay.
Report an error if the region is empty and NO-ERROR is nil."
  (fstar-subp-start)
  (let ((beg (fstar-subp--untracked-beginning-position))
        (end (save-excursion (goto-char end) (skip-chars-backward fstar--spaces) (point))))
    (if (<= end beg)
        (unless no-error
          (user-error "Nothing to process!"))
      (when (eq (char-after end) ?\n) ;; ←←← Here
        (cl-incf end))                ;; ←←← Here
      (fstar-assert (cl-loop for overlay in (overlays-in beg end)
                        never (fstar-subp-tracking-overlay-p overlay)))
      (let ((overlay (make-overlay beg end (current-buffer) nil nil)))
        (fstar-subp-remove-orphaned-issue-overlays (point-min) (point-max))
        (overlay-put overlay 'fstar-subp--lax fstar-subp--lax)
        (fstar-subp-set-status overlay 'pending)
        (fstar-subp--set-queue-timer)))))

[cpitclaudel]

Closing this; I'm not sure I dislike the current behavior, and I'd like more feedback before reverting that change.