From 8fdf9bf399ac4decf529f40cf55f0e570869f0f3 Mon Sep 17 00:00:00 2001 From: Yixuan Chen Date: Wed, 10 May 2023 15:04:02 -0400 Subject: [PATCH 1/2] advance-to-point advance to end of block --- fstar-mode.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/fstar-mode.el b/fstar-mode.el index 75bdcd1..371d65f 100755 --- a/fstar-mode.el +++ b/fstar-mode.el @@ -3485,9 +3485,9 @@ into blocks; process it as one large block instead." ((fstar-subp--in-tracked-region-p) (fstar-subp-retract-until (point))) ((consp arg) - (fstar-subp-enqueue-until (point))) + (fstar-subp-enqueue-until (save-excursion (fstar-subp-next-block-end) (point)))) (t - (fstar-subp-advance-until (point)))))) + (fstar-subp-advance-until (save-excursion (fstar-subp-next-block-end) (point))))))) (defun fstar-subp-advance-or-retract-to-point-lax (&optional arg) "Like `fstar-subp-advance-or-retract-to-point' with ARG, in lax mode." From 904a0a20ad1df2c326153ce1e82eed6f9e040836 Mon Sep 17 00:00:00 2001 From: Yixuan Chen Date: Wed, 10 May 2023 15:23:10 -0400 Subject: [PATCH 2/2] use the idempotent version instead --- fstar-mode.el | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/fstar-mode.el b/fstar-mode.el index 371d65f..f1e60f7 100755 --- a/fstar-mode.el +++ b/fstar-mode.el @@ -3485,9 +3485,9 @@ into blocks; process it as one large block instead." ((fstar-subp--in-tracked-region-p) (fstar-subp-retract-until (point))) ((consp arg) - (fstar-subp-enqueue-until (save-excursion (fstar-subp-next-block-end) (point)))) + (fstar-subp-enqueue-until (save-excursion (fstar-subp-next-block-start) (point)))) (t - (fstar-subp-advance-until (save-excursion (fstar-subp-next-block-end) (point))))))) + (fstar-subp-advance-until (save-excursion (fstar-subp-next-block-start) (point))))))) (defun fstar-subp-advance-or-retract-to-point-lax (&optional arg) "Like `fstar-subp-advance-or-retract-to-point' with ARG, in lax mode."