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

[Josh Tilles]

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 *problems* 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?)

Regardless, your replies were very useful to me. Thank you.


On Tue, Feb 4, 2014 at 4:25 AM, Lars Noschinski <noschinl at in.tum.de> wrote:

> 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
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140206/d9f783bc/attachment-0002.html>