如何让C-c C-n格式化proof-general coq-mode-map中的当前行

Question

我正在使用proof-general来编写Coq证明。

在校样中使用C-c C-n时，光标将移动到下一行，但当前行未格式化。例如，如果我键入：

intros n. <C-c C-n>

我的光标移动到下一行，但intros n.保持不缩进。因此，我必须返回一行，转到行尾，然后点击<RET>来自动缩进coq语句。在这一点上，proof-general认为该语句发生了变化，我必须重新运行它。

理想情况下，我会在C-c C-n行中自动缩进它正在运行的行，而不是转到下一行。

我怎样才能做到这一点呢？

Answer 1

你可以使用建议来做你所描述的事情：

(advice-add 'proof-assert-next-command-interactive :before
            (lambda (&rest args) (indent-for-tab-command)))

…但我怀疑这是一个AB问题：C-c C-n不会插入换行符，所以如果你正在写校样，你实际上每次按C-c C-n都会按一次RET。如果在按C-c C-n键之前按下它，则该行将正确缩进。

更糟糕的是，如果您使用的是默认设置(电缩进)，那么首先通常不应该有一个缩进错误的intros：任何导致intros需要缩进的父行都应该在创建它的行时导致它被缩进。

如果我误解了，请使用导致您需要此功能的场景的具体示例来更新OP，我们可以看到PG中是否已经有一些可能会有所帮助的东西。

Answer 2

我也在考虑@Clément建议的advice-add，但实际上我认为OP的建议与其说是一个功能愿望…，不如说是一个错误修复：

当我们在使用RET添加新行之前键入C-c C-n时，如果该行尚未正确缩进(如果此行是在编辑此行时而不是在之前的行上键入 RET 之后发生的，实际上可能会发生这种情况)，C-c C-n操作将被分散注意力地删除…所以我们需要重新做一次C-c C-n。

所以我刚刚在https://github.com/ProofGeneral/PG/pull/604，@azani和@clément中打开了一个试探性的公关:如果你有时间，请随时在那里发表评论/评论。