Isabelle/HOL中查看ML定义及PIDE跨文件跳转ML定义的方法

前置说明：<^binding>特殊语法的作用 #

你在示例中看到的<^binding>‹airspeed_velocity›属于Isabelle的ML反引用语法，不属于标准SML内容，作用是在ML代码块中直接生成一个绑定标识符，替代手写Binding.make的冗长写法，是Isabelle专门为ML层提供的语法糖。

ML文件内跳转失效的核心原因 #

从.thy文档通过Ctrl+Click跳转打开内置.ml源码文件时，PIDE默认会以无会话上下文关联的只读文本窗口形式加载文件，没有触发ML语法解析、符号索引生成流程，因此无法响应Binding.make、Scan.lift这类ML元素的跳转请求。

恢复跳转功能的操作步骤 #

• 不要直接使用跳转生成的只读窗口，打开当前运行Isabelle会话的工作区文件列表
• 通过会话的「打开文件」入口，定位到跳转目标路径下的ml_antiquotation.ml文件重新打开，让PIDE自动为该文件绑定当前会话的ML解析上下文
• 等待窗口右下角的解析进度完全完成后，即可对文件内所有ML元素使用Ctrl+Click触发定义跳转
• 若遇到内置ML文件为系统只读属性、无法被会话自动索引的情况，可将目标ML文件复制到当前理论项目的工作目录，在项目设置中将该目录挂载到会话的ML搜索路径，重新打开文件后即可获得完整跳转支持

独立SML文件的跳转支持范围 #

Isabelle PIDE的ML定义跳转功能存在明确的适用边界：

• 仅支持挂载到当前Isabelle会话、适配Isabelle配套PolyML语法的ML/SML文件，不对任意无关联的独立SML文件生效
• 未关联任何Isabelle会话路径的独立SML文件，会被PIDE识别为普通纯文本，不会触发语法解析、符号索引流程，和打开通用文本文件无差异
• 即使是挂载到会话路径下的SML文件，若存在和Isabelle适配版PolyML不兼容的语法，解析流程会直接报错，无法生成可跳转的符号索引

内容的提问来源于stack exchange，提问作者thor