Cannot process just comments

[tchajed]

VsCoq seems to never process just a comment. I think this is a bug.

If you're going through a file with large comments (e.g., in class), then it's possible to lose track of where the interpretation is up to is because the current view only has comments. In Proof General I step through those comments and can see exactly where that point is.

Processing the first comment in the file is also how I confirm that Coq has started and things are working, which doesn't do anything in VS Coq. This is true even with Proof Interpretation Mode set to NextCommand; you have to put the cursor on the non-comment part of the first sentence.

This also affects backtracking: if you backtrack before a command, it also reverts any comments before the command. This also leaves it unclear exactly where the backtracking went to, if it goes off screen. I'd prefer the comment remain processed.

[rtetley]

Thanks for your report ! To be clear: you want comments to behave like a "processable" command ? Meaning a step forward or backward on a comment will treat it like an executable sentence (from a UI perspective of course) ?

[TheoWinterhalter]

I would at best argue that this should be an opt-in because it doesn't make sense to me to process comments at all.

[gares]

Do we happen to make comments foldable? It could be a way to improve navigation without turning them into sentences, that would be very weird from the point of view of the document manager.

@tchajed do you show your students the comments? Or are there for them to read later? Would it work for you to fold them?

[SkySkimmer]

Having comments be pseudo-sentences work pretty well in PG IMO

[gares]

Coq's parser does not return them explicitly, so one would need to tweak the document parsing loop to inject toplevel comments as you go.

Anyway, everything is possible, but I think we should better understand the annoying workflow.

Clearly one does not want the cursor to be moved far back when stepping back a sentence. This may just be a side effect that currently sentences include preceeding comments, so the end of the prev sentence is the ., not the first non white space of the current sentence. This is fixable even without turning comments into sentences. eg The | signal sentence delimiters:

Definition foo := 3.|
(* bla *)
Definition bar := 4.|

We already know the position of the D after (* bla *), but maybe we don't use it to place the cursor after a step back from the second |. Am I right @rtetley ?

For the stepping forward it is a bit unclear to me what gets annoying. I let Tej elaborate.

[rtetley]

Currently we use the ranges of the sentence + the trailing white space before to compute the "overview" (green range).
In your example the range for the second sentence would be contained exactly between the two delimiters.
This is a change we introduced to avoid blanks between consecutive executed sentences (i.e. before this change the comments would have not been highlighted at all).

Concerning the comments, we do parse them at the moment, but they are kept in a separate data structure and are not treated as sentences.

[tchajed]

As far as I can recall this only affected me in class presentations. I would actually rather have a version for lecture that doesn't have these long comments (as Software Foundations does), which would solve the problem at its source. Folding all comments is a reasonable stop gap (which isn't working when I test it, not all comments can be folded).

Whether or not you think this is a reasonable feature, it is how Proof General works and I really appreciate it, that's why I opened an issue.

An annoying situation when processing forward is one like this (even if not presenting in class):

sentence1. (* the point is here *)
sentence2.
(* a very long comment taking half the screen *)
the sentence you're looking at.

In this file, you can't see where the interpretation point is, and it moves invisibly. If you try to move it to just after the long comment, it will work, but you won't see it working because the sentence isn't marked as processed. It is totally reasonable in my code to have a long comment and a sentence2. that takes several seconds to process.