Isabelle/jEdit-PIDE框架内的证明程序IDE
Isabelle/jEdit --- a Prover IDE within the PIDE framework
摘要：
PIDE是面向文档的证明器交互和集成的通用框架，基于结合ML和Scala的双语架构。总体目标是将LCF风格的证明器（如Isabelle或Coq或HOL）与JVM平台上的复杂前端技术连接起来，最终克服命令行交互。本系统描述特别涵盖Isabelle/jEdit，作为Isabelle 2011 -1（2011年10月）正式发布的一部分。它是一个具体的Prover IDE实现，一方面基于Isabelle/PIDE库模块（用Scala实现），另一方面基于著名的jEdit文本编辑器框架（用Java实现）。我们的Prover IDE的交互模型遵循连续证明检查的思想：理论源文本由prover在语义信息中进行注释，因为它逐渐变得可用。这通过异步协议工作，既不阻止编辑器也不阻止证明器在多核硬件上利用并行性。jEdit GUI为增强的文本编辑（突出显示、曲线、工具提示、超链接等）提供了标准的隐喻。我们已经从证明者上下文中检测出了形式内容。通过合适的插件和字体对jEdit显示引擎的进一步改进近似于文本缓冲区中的数学渲染，包括来自TeX指令表的符号和子/上标。Isabelle/jEdit在这里既作为当前Isabelle的可用接口，也作为参考应用程序，以激发基于PIDE的进一步项目。
英文摘要：
PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LCF-style provers like Isabelle (or Coq or HOL) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last. The present system description specifically covers Isabelle/jEdit as part of the official release of Isabelle2011-1 (October 2011). It is a concrete Prover IDE implementation based on Isabelle/PIDE library modules (implemented in Scala) on the one hand, and the well-known text editor framework of jEdit (implemented in Java) on the other hand. The interaction model of our Prover IDE follows the idea of continuous proof checking: the theory source text is annotated by semantic information by the prover as it becomes available incrementally. This works via an asynchronous protocol that neither blocks the editor nor stops the prover from exploiting parallelism on multi-core hardware. The jEdit GUI provides standard metaphors for augmented text editing (highlighting, squiggles, tooltips, hyperlinks etc.) that we have instrumented to render the formal content from the prover context. Further refinement of the jEdit display engine via suitable plugins and fonts approximates mathematical rendering in the text buffer, including symbols from the TeX repertoire, and sub-/superscripts. Isabelle/jEdit is presented here both as a usable interface for current Isabelle, and as a reference application to inspire further projects based on PIDE.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
