[isabelle-dev] How to use the Isabelle *release's* jEdit with the *repository* code?

[Lars Noschinski]

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

Isabelle2013-2.app/Contents/Resources/Isabelle2013-2/src/HOL/Finite_Set.thy

? 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.

   -- Lars

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 551 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140204/93cba546/attachment.sig>