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
find_theorems "_ < _" | <---- shows output
find_theorems "_ < _"
| <---- shows nothing
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
find_theorems "_ < _" | <---- shows output
find_theorems "_ < _"
| <---- shows nothing