-
Notifications
You must be signed in to change notification settings - Fork 285
Open
Labels
kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Description
Dafny version
4.11.0+fcb2042d6d043a2634f0854338c08feeaaaf4ae2
Code to produce this issue
method Abs(x: int) returns (y: int)
ensures x>=0 ==> x==y
ensures x < 0 ==> x+y==0
{
if x<0 {
return -x;
} else {
return x;
}
}
method test_abs(){
var a := Abs(-7);
assert(7 == a);
var b := Abs(7);
assert(7 == b);
}Command to run and resulting output
vscode
The colors should be preserved, after the first if if x<0 { everything bellow including unrelated functions are colored in blue.
What happened?
When editing a Dafny file, the syntax highlighting breaks if the comparison operator < has no spaces around it.
For example, the following function highlights correctly:
method Abs(x: int) returns (y: int)
ensures x >= 0 ==> x == y
ensures x < 0 ==> x + y == 0
{
if x < 0 {
return -x;
} else {
return x;
}
}However, if we remove the spaces around <, like this:
{
if x<0 {then the syntax highlighting of the rest of the file becomes entirely blue (as if the language grammar breaks).
Despite this, the Dafny verifier and execution still work correctly, the issue appears to affect only the syntax coloring.
Expected behavior
Removing spaces around operators should not affect syntax highlighting.
Actual behavior
Syntax highlighting breaks (the rest of the file turns blue), although verification and compilation remain functional.
What type of operating system are you experiencing the problem on?
Linux
Metadata
Metadata
Assignees
Labels
kind: bugCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` labelCrashes, unsoundness, incorrect output, etc. If possible, add a `part:` label