chore: add restartFile command #213
Conversation
|
@lovettchris Does the new command name and the explanation in the readme make it clearer what's going on? |
|
I see thanks, it is more clear to me now that this restarts the file worker, but I'm not sure it will be more clear to users that know nothing about what a file worker is. I think refreshFileDependencies is more "user centric" in terms of what it is usually used for. |
Note that the final version of this PR does not contain the words "file worker" anymore. It now only talks about "restarting server for a single file", which is hopefully understandable. |
|
Possibly https://github.com/leanprover/lean4/blob/dd924e5270fbe3b1c0ef739fd0601a7c3fc7745d/src/Lean/Server/README.md#recompilation-of-opened-files needs consideration of which spelling it should mention (right now it mentions refresh file dependencies obviously, but it sounds like restart file may by the preferred spelling now). |
|
Nice catch, "refresh file dependencies" is still there in vs code, it is just an alias for "restart file". But I did a bigger search and found "refresh file dependencies" is also mentioned in the quickstart.md, and on line 96 of the vscode-lean4 readme. It was not mentioned in TPIL or fp-lean books. I'll leave it to Gabriel to decide if we want to switch all mentions of "refresh file dependencies" over to the new name... |
No description provided.