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

Ask to load dependency theories #34

Open andriusvelykis opened 11 years ago

andriusvelykis commented 11 years ago

Currently if the opened theory imports some other non-heap theories, they are loaded automatically in the background.

Isabelle/jEdit asks the user whether these should be loaded, e.g. in case of large dependencies. Add similar functionality to Isabelle/Eclipse (at least a preference if background-loading is preferred).

See isabelle.eclipse.ui.editors.TheoryEditor.State#loadTheoryImports().

makarius commented 11 years ago

Note that this behaviour in Isabelle/jEdit is just a cheap way to populated the document model, without requiring a second store for theory nodes independently of editor buffers. I would prefer silent implicit loading, and hope to provide some general Isabelle/Scala functionality for that eventually.