>我一直在创建一个Web IDE（WIDE）来证明计算机科学中的定理。您可能知道，有 3 种最常见的证明助手，它们命名为雅典娜、伊莎贝尔和科克。大多数计算机科学家可能会忘记他们的语法、范围等。我的 Web IDE 使用拖放设计和示例。您可以在其上编辑和编写其他代码，可以下载，可以共享，可以保存等。它也有自己的解析器。到目前为止一切正常。小心！这是我的问题：当用户想在我的 Web IDE 上运行他们的代码时，我如何运行用户的代码并获得结果（特别是对于 Athena http://proofcentral.org/）。实际上，我可以通过 mouse_event （user32） 和其他带有 pinvoke（平台调用）的来做到这一点。我的程序通过Web将代码发送到正在运行的PC（而不是服务器。因为服务器没有屏幕，所以程序不会知道点击到哪里），然后PC得到代码。然后程序点击到"emacs"图标。几秒钟后（用于打开和上传 Athena 的 dll），程序将 Athena 代码粘贴到 emacs shell 中。Emacs 运行该代码并返回结果。之后，程序选择，复制结果并将其返回到Web IDE。然而，这是一种怪异而棘手的方式。我想做最好的方法。感谢您的关注。最好
我只能给伊莎贝尔一个部分答案：
Isabelle本身是用标准ML实现的，但为了与外部世界进行通信，它使用了一种称为PIDE（= Prover IDE）的协议。PIDE的参考实现与Isabelle捆绑在一起，并用Scala编写，因此它可以与任何JVM语言一起使用。PIDE的主要应用是Isabelle/jEdit，它使用jEdit编辑器为Isabelle构建IDE，包括标记，连续检查，...
还有其他IDE，如Isabelle/Eclipse和Clide（基于Web）。对于您的用例，Clide 似乎高度相关。
如果您想了解更多关于PIDE的内部工作原理，可以查阅Wenzel的相关论文，例如Isabelle/PIDE中的异步用户交互和工具集成以及Isabelle作为面向文档的证明助手。
现在，终于，无耻的插件：由于如何与Isabelle作为外部程序进行交互的问题时不时地出现，我将PIDE与一些额外的实用程序打包为libisabelle。它包括一个非常简单的乒乓球与证明者交互的示例。