2023-08-16 17:08:31 +02:00
|
|
|
syntax = "proto3";
|
|
|
|
|
|
|
|
package codemp.cursor;
|
|
|
|
|
2023-08-20 07:32:08 +02:00
|
|
|
// handle cursor events and broadcast to all users
|
2023-08-16 17:08:31 +02:00
|
|
|
service Cursor {
|
2023-08-20 07:32:08 +02:00
|
|
|
// send cursor movement to server
|
2023-08-16 23:09:47 +02:00
|
|
|
rpc Moved (CursorEvent) returns (MovedResponse);
|
2023-08-20 07:32:08 +02:00
|
|
|
// attach to a workspace and receive cursor events
|
2023-08-16 23:09:47 +02:00
|
|
|
rpc Listen (UserIdentity) returns (stream CursorEvent);
|
2023-08-16 17:08:31 +02:00
|
|
|
}
|
|
|
|
|
2023-08-20 07:32:08 +02:00
|
|
|
// empty request
|
2023-08-16 17:08:31 +02:00
|
|
|
message MovedResponse {}
|
|
|
|
|
2023-08-20 07:32:08 +02:00
|
|
|
// a tuple indicating row and column
|
2023-08-16 23:09:47 +02:00
|
|
|
message RowCol {
|
2023-08-16 17:08:31 +02:00
|
|
|
int32 row = 1;
|
|
|
|
int32 col = 2;
|
|
|
|
}
|
|
|
|
|
2023-08-20 07:32:08 +02:00
|
|
|
// cursor position object
|
2023-08-16 17:08:31 +02:00
|
|
|
message CursorPosition {
|
2023-08-20 07:32:08 +02:00
|
|
|
// path of current buffer this cursor is into
|
2023-08-16 23:09:47 +02:00
|
|
|
string buffer = 1;
|
2023-08-20 07:32:08 +02:00
|
|
|
// cursor start position
|
2023-08-16 23:09:47 +02:00
|
|
|
RowCol start = 2;
|
2023-08-20 07:32:08 +02:00
|
|
|
// cursor end position
|
2023-08-16 23:09:47 +02:00
|
|
|
RowCol end = 3;
|
|
|
|
}
|
|
|
|
|
2023-08-20 07:32:08 +02:00
|
|
|
// cursor event, with user id and cursor position
|
2023-08-16 23:09:47 +02:00
|
|
|
message CursorEvent {
|
2023-08-20 07:32:08 +02:00
|
|
|
// user moving the cursor
|
2023-08-16 17:08:31 +02:00
|
|
|
string user = 1;
|
2023-08-20 07:32:08 +02:00
|
|
|
// new cursor position
|
2023-08-16 23:09:47 +02:00
|
|
|
CursorPosition position = 2;
|
2023-08-16 17:08:31 +02:00
|
|
|
}
|
|
|
|
|
2023-08-20 07:32:08 +02:00
|
|
|
// payload identifying user for cursor attaching
|
2023-08-16 17:08:31 +02:00
|
|
|
message UserIdentity {
|
2023-08-20 07:32:08 +02:00
|
|
|
// user identifier
|
2023-08-16 17:08:31 +02:00
|
|
|
string id = 1;
|
|
|
|
}
|