我看到的大多数 Isabelle 文档都说 Proof-General 支持 Isabelle，但据我所知 PG 大约 5 年前就放弃了支持。
是否还有另一种可能性可以在 Emacs 中使用（当前的）Isabelle？JEdit 和 VSCode 都不适合我。
小智 6
没有官方的解决方案，也没有办法让 Proof General 再次发挥作用。
不过，有一个非官方的解决方案。你可以试试isabelle-emacs（免责声明：我在空闲时间开发的，体验有点粗糙，但是有几个人使用它）。它像 VScode 一样使用 Isabelle 的 LSP 服务器，但它使用基于 Emacs 的。isabelle-emacs 和 Isabelle 之间的差异仅限于 LSP 服务器中的几行和 Emacs 特定代码。内核或任何其他理论都没有改变。