在 Isabelle/jEdit 中处理理论而不保存它

Question

在 Isabelle/jEdit 中，有时我只想在一次性理论中测试一些东西，而不是将其保存到磁盘。但是当我创建一个新文件时（即使使用模式设置为 isabelle 的 new in mode 命令），在我保存它之前不会处理缓冲区（使用适当的文件名）。

有没有办法保存文件？看起来这应该是可能的，因为默认情况下 Isabelle/jEdit 以一个空的 Scratch.thy 文件开始，即使它没有被保存，它也会被处理。

Answer 1

Isabelle/jEdit 似乎使用缓冲区名称来决定是否处理一个理论（必须以.thy 结尾）。据我所知，jEdit 不提供更改缓冲区名称而不保存它的方法。但是，您可以打开一个不存在的文件，生成的缓冲区将以该文件命名。

因此，无需创建新文件，只需打开一个不存在的文件（当然，名称以 .thy 结尾），即使未保存到磁盘，Isabelle/jEdit 也会对其进行处理。