2

When I try and copy paste proof code, sometimes a [...] will show up (even though I did not copy anything of the kind) and I cannot delete it. I have to undo the copy in order to get rid of it. What does this mean?

Thanks.

push33n
  • 398
  • 4
  • 12
  • I have not encountered this issue before... What version of PG are you using? Can you reproduce the error unconditionally, or does it arise purely by luck? – Arthur Azevedo De Amorim May 11 '20 at 21:03
  • Do you use [company-coq](https://github.com/cpitclaudel/company-coq)? if yes, maybe this is just the [code folding feature](https://github.com/cpitclaudel/company-coq/blob/master/img/folding.gif)? – ErikMD May 11 '20 at 21:57
  • I can't manage to reproduce it, but it has happened to me twice before. It always happens when I am copy pasting code from one proof into a different proof that is still in progress, but unfortunately I cannot give you more details than that. My version of PG is 4.5 and my version of emacs is 24.3. – push33n May 11 '20 at 22:01
  • @ErikMD that's exactly what it is! Thank you! – push33n May 11 '20 at 22:02

1 Answers1

3

As confirmed in the comments, the occurrences of […] correspond here to the code folding feature of company-coq.

To toggle the visibility of a block (starting with a brace, e.g.

Goal True /\ True.
split.
{ […]

or starting with a bullet, e.g.

Goal True /\ True.
split.
- idtac. […]

), you can just move the point to the opening symbol { or -, and press RET

Otherwise, to "unfold" all blocks of the ambient buffer, you can do:

M-x company-coq-features/code-folding-reset-to-initial-state RET

ErikMD
  • 13,377
  • 3
  • 35
  • 71