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

Go to definition does not work properly if theory not loaded #28

Closed andriusvelykis closed 11 years ago

andriusvelykis commented 11 years ago

Open a theory B that imports another theory A in the project (i.e. not Main) but without opening A first. Open a hyperlink to a definition defined in A: the editor is opened with A, but the cursor is at the top of the editor, not on the definition. Subsequent jump with the editor open works correctly and highlights the definition.

andriusvelykis commented 11 years ago

Fixed by avoiding theory reload if A is already submitted (issue #29)