【发布时间】：2020-10-21 12:39:16
【问题描述】：
假设我记得一个常数或理论名称，但完全忘记了它是在哪里声明的。也许，我什至不知道它是在哪个 MMT 存档中声明的。如何找到源文件？
我可以只打开一个 MMT shell，加载我磁盘上的所有档案，然后发出一些命令find_constant <constant name> 吗？有这样的命令吗？
【问题讨论】：
标签： development-environment mmt
【发布时间】：2020-10-21 12:39:16
【问题描述】：
这取决于你对你所寻求的声明点的了解：
-
如果您什么都不知道，即如果您甚至没有使用该事物的类型检查文件。
那么找出声明点的最简单方法就是使用正则表达式对所有
*.mmt文件进行 grep。对于（类型化的）常量，使用<constant name>\s*?:。它将匹配常量声明，后跟一些可选的空格和冒号。使用 Notepad++，这很容易做到。比如说，你想知道
congT是在哪里声明的。然后你会这样做： -
您有一个类型检查 MMT 文件，其中使用了您要查找的内容。
然后使用MMT IntelliJ plugin 及其文档树：首先对手头的文件进行类型检查，然后在 Sidekick 中查找常量的出现：
激活 Navigate 选项在这里特别有用：您只需用鼠标单击您要寻找的声明点（例如
nat_lit）并立即将其显示在搭档。在这里，sidekick 显示nat_lit (?NatLiterals)，这意味着该常量是在理论NatLiterals中定义的。理想情况下，您知道该理论的声明位置。理论上，您也可以按住 Control 键单击常量，但目前由于我不知道的原因，这不起作用。
【讨论】：