<div dir="ltr">The details of packaging jEdit & why it appears different depending on my invocation are still mysterious to me, but when I just tried to reproduce the <i>problems</i> I was having, I was unable to. (Perhaps the limitation was on a previous version of Isabelle and I've just been working around it since then?)<div>

<br></div><div>Regardless, your replies were very useful to me. Thank you.</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Feb 4, 2014 at 4:25 AM, Lars Noschinski <span dir="ltr"><<a href="mailto:noschinl@in.tum.de" target="_blank">noschinl@in.tum.de</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 04.02.2014 01:05, Josh Tilles wrote:<br>
> Essentially, how do you configure Isabelle/jEdit when you want to make<br>
> changes to the "core" logics? (e.g., HOL, or even Pure)<br>
<br>
</div>I don't think you can interactively make changes to Pure -- the protocol<br>
which is used by Isabelle/jEdit to communicate with the Isabelle core is<br>
part of Pure.<br>
<div class="im"><br>
> IF YOU NEED MORE DETAILS:<br>
> I'm using Isabelle2013-2 on Mac OS X.<br>
> If I naively open Isabelle2013-2.app, I'm unable to work with files from<br>
> the repository because jEdit tells me that I already have theories<br>
> loaded with that name.<br>
<br>
</div>That is normal.<br>
<div class="im"><br>
> However, if I run `bin/isabelle jedit` in the repository, then jEdit<br>
> looks very different when it opens and seems poorly configured.<br>
<br>
</div>This might be a packaging issue on OS X; in general, running<br>
"bin/isabelle jedit" is a supported way of using Isabelle/jEdit.<br>
<div class="im"><br>
> So if I attempt to run<br>
> `Isabelle2013-2.app/Contents/Resources/Isabelle2013-2/bin/isabelle jedit<br>
> -l Pure` and then open the repository's src/HOL/Finite_Set.thy, jEdit<br>
> can't find Finite_Set's dependencies!<br>
<br>
</div>This is the correct way of doing it -- I suppose you are trying to open<br>
<br>
Isabelle2013-2.app/Contents/Resources/Isabelle2013-2/src/HOL/Finite_Set.thy<br>
<br>
? You should get a popup window asking you whether to load the<br>
dependencies. I minor gotcha is that jEdit continues to complain about<br>
missing theories, until it has processed all of the dependencies. You<br>
can follow the progress in the "Theories" tab.<br>
<span class="HOEnZb"><font color="#888888"><br>
   -- Lars<br>
<br>
</font></span><br>_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br>
<br></blockquote></div><br></div>