Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Problems importing files on-the-fly #68

Open
andriusvelykis opened this issue Apr 17, 2013 · 1 comment
Open

Problems importing files on-the-fly #68

andriusvelykis opened this issue Apr 17, 2013 · 1 comment
Labels
Milestone

Comments

@andriusvelykis
Copy link
Owner

Theory imports are not loaded when typing on-the-fly and the error message remains even after restarting the editor.

To reproduce: create a new file Scratch.thy and start typing:

theory Scratch
imports Main "~~/src/HOL/Library/RBT"
begin

end

This results in an error: Bad theory file (file
"file:/home/necoro/isabelle/Isabelle2013/src/HOL/Library/RBT.thy")

The dependencies can be loaded after closing and re-opening the editor. However the error remains.

Investigate better loading on-the-fly as well as why the error is persistent.

@andriusvelykis
Copy link
Owner Author

Looks like the issue is releated with the error marker not being deleted. After editor reloading, the theory is loaded correctly (see tick in the Theories view), but the marker is not deleted.

A workaround is to delete the marker in Problems view for now. Need to check why the marker is not removed..

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant