Cleaning up whitespace shouldn't require rewinding

[proofgeneral]

Cleaning up whitespace shouldn't require rewinding

[JasonGross]

Here is some code that runs correctly before stripping trailing spaces, but fails after stripping them:

Require Import Coq.Strings.String.
Definition foo := "    
"%string.
Check eq_refl : String.length foo = 5.

[Matafou]

Let us try this for a while and see.

While you ar at it, indenting should not rewind either.

Spaces are (very) significant when following a dot ([Foo. bar] is different
than [Foo.bar]). To my knoledge (and excepting strange stuff with notation
maybe) this is the only significant space.

P.

2015-10-09 1:06 GMT+02:00 Clément Pit--Claudel [email protected]:

In most cases (in all?), removing extra whitespace at the end of a line
shouldn't require rewinding; even outside of comments. Yet at the moment
calling whitespace-cleanup will cause PG to rewind to the earliest point
where some space was removed.

This is a bit frustrating, so I'd like to push a patch to suppress the
rewinding behaviour when removing space at the end of the line. Are there
objections?

Also, what should be the proper behaviour? Do we allow insertion of spaces
as well? Only at the end of lines? Or anywhere outside of strings and
outside of symbols? (is space significant anywhere in Coq?)

—
Reply to this email directly or view it on GitHub
#4.

[cpitclaudel]

Some notes after having a quick look: this isn't trivial, because retracting is implemented as a before-change hook, which doesn't convey information on the text about to be inserted or deleted. Using an after-change-hook would work better.

Interesting functions to look at: span-write-warning and proof-span-read-only and proof-retract-before-change.

[Matafou]

Writing seems more difficult before setting readonly off than before indeed!
P.

Le lundi 23 novembre 2015, Clément Pit--Claudel [email protected]
a écrit :

Some notes after having a quick look: this isn't trivial, because
retracting is implemented as a before-change hook, which doesn't convey
information on the text about to be inserted or deleted. Using an
after-change-hook would work better.

Interesting functions to look at: span-write-warning and
proof-span-read-only and proof-retract-before-change.

—
Reply to this email directly or view it on GitHub
#4 (comment).

[JasonGross]

Outside of string literals, I believe that Coq treats one whitespace character the same as any positive number of whitespace characters. So adding or removing whitespace at a location bordered by whitespace (and a newline counts as whitespace) should be safe as long as you're not in the middle of a string literal (and these are used in format modifiers for notations, too). (Dots are not special in that whitespace around them matters (in some sense, other characters are special in that whitespace around them usually does not matter); e.g., f oo is very different from foo.)

[cpitclaudel]

Spaces in strings are a good point, thanks! There are technical challenges with this due to the way retraction is implemented though, so I'm not sure when or if it will happen.

[JasonGross]

Note that undo (C-/) edits arbitrary regions without retraction (incorrectly!), so, in some sense, there must be a way to bypass retraction, no?

[cpitclaudel]

Undo reverts fine for me. Are you using an undo package? If not, can you post a recipe?

There's definitely a way to bypass restriction (it's used, for example, when you edit text inside a comment); the hard part is deciding when to bypass it.