无法在Isabelle/jEdit中选择已构建的会话映像

Question

这是对

loading a precompiled heap image in Isabelle

现在我在Windows上。我在标准位置创建了一个Nominal2堆映像：

$HOME/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin

我不能在理论面板中选择它来加载。

我试图从一个cygwin脚本启动isabelle jedit -d ... -l ...，但这是行不通的。包含的脚本

#!/bin/bash

isabelle jedit -d /cygdrive/d/phd/thy/Nominal2-Isabelle2015/Nominal  -l Nominal2

但是我什么都没做，jEdit没有出现。

如何创建自动加载预构建的Nominal2映像的可执行文件？或者，让Isabelle/jEdit知道标准堆位置中有一个Nominal2映像？

更新:我将图像从用户的主目录复制到主堆目录：

in /cygdrive/d/isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin 

$ cp ~/.isabelle/Isabelle2015/heaps/polyml-5.5.2_x86-cygwin/Nominal2 .

并重新启动了Isabelle/jEdit，但是我在菜单中找不到会话图像的Nominal2。

Answer 1

与其尝试手工组装堆映像并移动它们，还不如让系统来完成它。您只需通过isabelle jedit -d DIR或通过某些根文件(在一些已知的会话目录中)，告诉它在哪里找到会话源树。

一个很好的地方是$ISABELLE_HOME_USER/ROOTS：只需将目录位置(在Isabelle/POSIX符号中)添加到单独的行中，而Isabelle/jEdit逻辑选择器在重新启动后应该知道新的会话。

然后您可以选择一个新会话，它的堆将在应用程序下一次重新启动后生成。