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

Avoid re-initialising theory if already submitted #29

Closed andriusvelykis closed 11 years ago

andriusvelykis commented 11 years ago

When a theory with imports is opened, its imported theories (dependencies) are currently automatically submitted to Isabelle prover. Now if the editor on these theories is opened again, the theory contents are re-submitted fully to the prover.

This is unnecessary, since it requires re-running all proofs in the dependency theory as well as in all theories that import it. Instead, check if the theory is already submitted and just use the snapshot version (react to subsequent edits of course).