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

Last error in theory gets "stuck" #55

Closed makarius closed 11 years ago

makarius commented 11 years ago

Consider this example:

theory Test
imports Main
begin

term "x x"

It produces an error with read indicator in the last line. Removing the characters of that line, the red icon on left left remains. It disappears only after adding good text in this last line.

andriusvelykis commented 11 years ago

Thanks - good catch. I operated with wrong assumption that Isabelle sent a command change event even if the command was actually deleted altogether. Fixed this - should be working ok now...