Re: [isabelle] Isabelle/{jEdit, Eclipse} problem with importing files



Hi,

I can confirm this problem at least in the case of Isabelle/Eclipse -
thanks for reporting.

In Isabelle/Eclipse dependencies are currently only loaded during editor
initialisation. You can achieve "reloading" by saving and re-opening the
editor. This way the dependencies are loaded correctly.

The problem is that the error marker still lingers. This is a bug on my
side, because the theory is loaded correctly (you can see the "success" in
Theories view if you finish with your theory with "end"). As a workaround,
you can manually delete the error marker in Problems view (right-click >
Delete) and it will not reappear.

I have filed this issue in Isabelle/Eclipse:
http://github.com/andriusvelykis/isabelle-eclipse/issues/68

Thanks,
Andrius




On Wed, Apr 17, 2013 at 2:20 PM, René Neumann <rene.neumann at in.tum.de>wrote:

> Hi,
>
> I have the same error in Isabelle/jEdit and Isabelle/Eclipse (therefore,
> I think, it lies in the layer beneath):
>
> Just typing
>
> theory Scratch
> imports Main "~~/src/HOL/Library/RBT"
> begin
>
> results in "Bad theory file (file
> "file:/home/necoro/isabelle/Isabelle2013/src/HOL/Library/RBT.thy")
>
> If I (somehow) manage to trick jEdit into a reload (don't know how to do
> it with Eclipse), it eventually is able to load it.
>
> - René
> --
> René Neumann
>
> Institut für Informatik (I7)
> Technische Universität München
> Boltzmannstr. 3
> 85748 Garching b. München
>
> Tel: +49-89-289-17232
> Office: MI 03.11.055
>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.