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

Do not load pre-loaded heap theories #14

Closed andriusvelykis closed 11 years ago

andriusvelykis commented 11 years ago

Hyperlinks to Isabelle constant definitions in the heap (e.g. Set) open editors for these theory files. Since the heap is already loaded, re-submitting the theory file them produces an error.

Avoid submitting pre-loaded heap theories - treat them as read-only files instead to avoid this error being reported.

andriusvelykis commented 11 years ago

Implemented in bf2f3257bd4f9c6f9c7fc95cc0dc54d21b9f3bd0

The loaded theories are available in ThyLoad. They are checked - if the theory is already loaded, a read-only version of editor is initialised.

Note that this editor does not have a Snapshot of prover results underneath, thus Prover Output view does not display anything. Furthermore, semantic highlighting (e.g. variable colours) also is not available for the same reason. However, basic command-level syntax highlighting and parsed Outline works.