[isabelle-dev] How to use the Isabelle *release's* jEdit with the *repository* code?
noschinl at in.tum.de
Tue Feb 4 10:25:40 CET 2014
On 04.02.2014 01:05, Josh Tilles wrote:
> Essentially, how do you configure Isabelle/jEdit when you want to make
> changes to the "core" logics? (e.g., HOL, or even Pure)
I don't think you can interactively make changes to Pure -- the protocol
which is used by Isabelle/jEdit to communicate with the Isabelle core is
part of Pure.
> IF YOU NEED MORE DETAILS:
> I'm using Isabelle2013-2 on Mac OS X.
> If I naively open Isabelle2013-2.app, I'm unable to work with files from
> the repository because jEdit tells me that I already have theories
> loaded with that name.
That is normal.
> However, if I run `bin/isabelle jedit` in the repository, then jEdit
> looks very different when it opens and seems poorly configured.
This might be a packaging issue on OS X; in general, running
"bin/isabelle jedit" is a supported way of using Isabelle/jEdit.
> So if I attempt to run
> `Isabelle2013-2.app/Contents/Resources/Isabelle2013-2/bin/isabelle jedit
> -l Pure` and then open the repository's src/HOL/Finite_Set.thy, jEdit
> can't find Finite_Set's dependencies!
This is the correct way of doing it -- I suppose you are trying to open
? You should get a popup window asking you whether to load the
dependencies. I minor gotcha is that jEdit continues to complain about
missing theories, until it has processed all of the dependencies. You
can follow the progress in the "Theories" tab.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 551 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev