remoting: Edit dev server (#11344)

This PR allows configuring existing dev server, right now you can:
- Change the dev servers name
- Generate a new token (and invalidate the old one)

<img width="563" alt="image"
src="https://github.com/zed-industries/zed/assets/53836821/9bc95042-c969-4293-90fd-0848d021b664">


Release Notes:

- N/A
This commit is contained in:
Bennet Bo Fenner 2024-05-06 12:58:11 +02:00 committed by GitHub
parent 6e2be283dd
commit 593f0e0c3e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 697 additions and 209 deletions

View file

@ -323,6 +323,9 @@ messages!(
(ValidateDevServerProjectRequest, Background),
(DeleteDevServer, Foreground),
(DeleteDevServerProject, Foreground),
(RegenerateDevServerToken, Foreground),
(RegenerateDevServerTokenResponse, Foreground),
(RenameDevServer, Foreground),
(OpenNewBuffer, Foreground)
);
@ -430,6 +433,8 @@ request_messages!(
(MultiLspQuery, MultiLspQueryResponse),
(DeleteDevServer, Ack),
(DeleteDevServerProject, Ack),
(RegenerateDevServerToken, RegenerateDevServerTokenResponse),
(RenameDevServer, Ack)
);
entity_messages!(