-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix: Formatting on VSCode for multi-file projects with project file #4918
Changes from 3 commits
274f26e
8b95924
3fbe6d1
733030c
39cbb3b
b669fa1
fff8129
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -23,11 +23,14 @@ public IndentationFormatter(TokenNewIndentCollector formatter) { | |
/// Creates an IndentationFormatter for the given program, | ||
/// by immediately processing all nodes and assigning indentations to most structural tokens | ||
/// </summary> | ||
public static IndentationFormatter ForProgram(Program program, bool reduceBlockiness = true) { | ||
var tokenNewIndentCollector = new TokenNewIndentCollector(program) { | ||
public static IndentationFormatter ForProgram(Program program, Uri uri, bool reduceBlockiness = true) { | ||
var tokenNewIndentCollector = new TokenNewIndentCollector(program, uri) { | ||
ReduceBlockiness = reduceBlockiness | ||
}; | ||
foreach (var child in program.DefaultModuleDef.PreResolveChildren) { | ||
if (child.Tok.line != 0 && child.Tok.Uri != uri) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
continue; | ||
} | ||
if (child is TopLevelDecl topLevelDecl) { | ||
tokenNewIndentCollector.SetDeclIndentation(topLevelDecl, 0); | ||
} else if (child is Include include) { | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -83,8 +83,9 @@ private Indentations PosToIndentations(int pos) { | |
public int binOpIndent = -1; | ||
public int binOpArgIndent = -1; | ||
|
||
internal TokenNewIndentCollector(Program program) { | ||
internal TokenNewIndentCollector(Program program, Uri uri) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What uri is this? My impression is that you want to format one file at a time, which is fine, but let's make that explicit by renaming |
||
this.program = program; | ||
this.uri = uri; | ||
preResolve = true; | ||
} | ||
|
||
|
@@ -222,6 +223,7 @@ public int GetRightAlignIndentAfter(IToken token, int indentFallback) { | |
} | ||
|
||
private static readonly Regex FollowedByNewlineRegex = new Regex("^[ \t]*([\r\n]|//)"); | ||
private readonly Uri uri; | ||
|
||
public static bool IsFollowedByNewline(IToken token) { | ||
return FollowedByNewlineRegex.IsMatch(token.TrailingTrivia); | ||
|
@@ -231,7 +233,7 @@ public static bool IsFollowedByNewline(IToken token) { | |
// 'inline' is the hypothetical indentation of this token if it was on its own line | ||
// 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation | ||
public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) { | ||
if (token.FromIncludeDirective(program) || (token.line == 0 && token.col == 0)) { | ||
if (token.Uri != uri || (token.line == 0 && token.col == 0)) { | ||
// Just ignore this token. | ||
return; | ||
} | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -596,6 +596,7 @@ public static void WriteFile(string filename, string text, string moreText = nul | |
if (moreText != null) { | ||
target.Write(moreText); | ||
} | ||
target.Close(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Does the above using directive not already guarantee that target is closed? This line seems obsolete. |
||
} | ||
|
||
private static void CheckFilenameIsLegal(string filename) { | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not OK for performance reasons. We need to design our code towards parsing in a streaming fashion. Could you take this part out for now so we can fix #4836 ASAP?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I usually worry more about correctness than performance, but I think I might find something that suits both of our needs and I'll put it up in a separate PR.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was about to write a StreamReader that auto-closes the file it reads when done, since I haven't found any. However, after analzying the code further, I don't think it is necessary.
Here is an analysis to consider:
IFileSystem.cs:50 public TextReader ReadFile(Uri uri) {
is called byDafnyProject.cs:53
which has aReadToEndAsync
but does not closes the streamIFileSystem.cs:25 public TextReader ReadFile(Uri uri) {
which has the same usage as its parentsLanguageServerFileSystem.cs:41 existingText = OnDiskFileSystem.Instance.ReadFile(uri).ReadToEnd();
which reads to the end but does not closes the streamLanguageServerFileSystem:92
which has the same usage as its parentsDafnyFile.cs:96
store the call as a closure in theGetContent
of a field of aDafnyFile
. This field is read in different places:ProgramParser.cs:269
var text = SourcePreprocessor.ProcessDirectives(getReader(), new List<string>());
which returns a source file after preprocessing. as a single string, but does not close the streamCoverageReporter.cs:321
var source = dafnyFile.GetContent().ReadToEnd();
reads to the end but does not close the streamFormatCommand.cs:75
using var content = dafnyFile.GetContent(); var originalText = await content.ReadToEndAsync();
This one also reads to the end and close the stream appropriately (I don't remember doing that, probably you did when you migrate to the new file system, so thanks)In short, we currently never rely on streaming files and just forget to close it in almost every place. C# does perform auto-closing but is lazy and for big files it won't do it fast enough, which crashes the formatter on the command-line randomly.
So my recommandation is just to do this read and close it immediately so that it becomes possible to write after read. I'll create a separate PR for that.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
#4950
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What makes you say it does not close the stream? It uses a
using
directive:Regarding the rest of the list, good finds! Let's fix them.