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


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:


On Wed, Apr 17, 2013 at 2:20 PM, René Neumann <rene.neumann at>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.