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

[Josh Tilles]

Following up with the solution:
Instead of the default value of `javax.swing.plaf.nimbus.NimbusLookAndFeel`, replace the `lookAndFeel` property’s default value with `com.apple.laf.AquaLookAndFeel`. There are other, smaller, differences in packaging too, but this makes the repository’s jEdit
feel “normal” on a Mac.

On Feb 6, 2014, at 2:00 PM, Josh Tilles <merelyapseudonym at gmail.com> wrote:

> 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/20140221/8d849a49/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140221/8d849a49/attachment.sig>