search

andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Problems importing files on-the-fly #68

Open andriusvelykis opened 11 years ago

andriusvelykis commented 11 years ago

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 commented 11 years ago

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..