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

Some unfinished annotations remain in the editor #22

Closed andriusvelykis closed 11 years ago

andriusvelykis commented 11 years ago

Sometimes arbitrary commands in the Isabelle theory editor remain with red annotations (unfinished) even though the prover completes the work. If selected, the prover output is displayed in Prover Output view and the command seems to have finished, however the annotations are not removed.

This is hard to reproduce and happens sporadically - points to a race condition somewhere.

andriusvelykis commented 11 years ago

Fixed in f1a78e4460c251987ffb94094bff09d3bf6252a3

There does seem to be a race condition in AnnotationModel (see this StackOverflow question for similar account).

Fixed by calling invalidateTextPresentation on the SourceViewer after setting the annotations.

Also streamlined events in annotation creation a bit.