hexedtech/codemp
3
0
Fork 0
mirror of https://github.com/hexedtech/codemp.git synced 2024-10-22 17:59:20 +02:00
Code Issues Projects Releases Packages Wiki Activity Actions

chore: public workspace event type

Browse source
This commit is contained in:
zaaarf 2024-10-15 22:36:43 +02:00
parent 3bf620d41a
commit 96a8b1a88f
No known key found for this signature in database
GPG key ID: 102E445F4C3F829B
1 changed files with 19 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
dist/java/src/mp/code/Workspace.java vendored
View file

@ -4,6 +4,7 @@ import java.util.Optional;
import java.util.UUID; import java.util.UUID;
import java.util.function.Consumer; import java.util.function.Consumer;
import lombok.Getter;
import mp.code.exceptions.ConnectionException; import mp.code.exceptions.ConnectionException;
import mp.code.exceptions.ConnectionRemoteException; import mp.code.exceptions.ConnectionRemoteException;
import mp.code.exceptions.ControllerException; import mp.code.exceptions.ControllerException;
@ -232,7 +233,8 @@ public final class Workspace {
* Represents a workspace-wide event. * Represents a workspace-wide event.
*/ */
public static final class Event { public static final class Event {
private final Type type; /** The type of the event. */
public final @Getter Type type;
private final String argument; private final String argument;
Event(Type type, String argument) { Event(Type type, String argument) {
@ -270,9 +272,24 @@ public final class Workspace {
} else return Optional.empty(); } else return Optional.empty();
} }
enum Type { /**
* The type of workspace event.
*/
public enum Type {
/**
* Somebody joined a workspace.
* @see #getUserJoined() to get the name
*/
USER_JOIN, USER_JOIN,
/**
* Somebody left a workspace
* @see #getUserLeft() to get the name
*/
USER_LEAVE, USER_LEAVE,
/**
* The filetree was updated.
* @see #getChangedBuffer() to see the buffer that changed
*/
FILE_TREE_UPDATED FILE_TREE_UPDATED
} }
} }