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

Editor issues #78

Open leouk opened 11 years ago

leouk commented 11 years ago

Using the editor now with PP enabled I get some issues (which I think are general).

The clipboard gets out of synch sometimes (on Mac). Cmd-C copies Cmd-V pastes okay. Then if I do another Cmd-C Cmd-V it keeps the old clipboard contents.

The prover output window has some strange behaviours too. Sometimes the display only occurs after you do a newline, whereas others it only appears at the end of the line. ex, assuming "|" is the cursor.

apply safe | <--- shows nothing

apply safe \n
| <---- shows output

findtheorems " < _" | <---- shows output

findtheorems " < _"
| <---- shows nothing