From 96a8b1a88fb9e33f11adde952773a915639b2951 Mon Sep 17 00:00:00 2001
From: zaaarf <me@zaaarf.foo>
Date: Tue, 15 Oct 2024 22:36:43 +0200
Subject: [PATCH] chore: public workspace event type

---
 dist/java/src/mp/code/Workspace.java | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/dist/java/src/mp/code/Workspace.java b/dist/java/src/mp/code/Workspace.java
index 10ae3b1..2d82192 100644
--- a/dist/java/src/mp/code/Workspace.java
+++ b/dist/java/src/mp/code/Workspace.java
@@ -4,6 +4,7 @@ import java.util.Optional;
 import java.util.UUID;
 import java.util.function.Consumer;
 
+import lombok.Getter;
 import mp.code.exceptions.ConnectionException;
 import mp.code.exceptions.ConnectionRemoteException;
 import mp.code.exceptions.ControllerException;
@@ -232,7 +233,8 @@ public final class Workspace {
 	 * Represents a workspace-wide event.
 	 */
 	public static final class Event {
-		private final Type type;
+		/** The type of the event. */
+		public final @Getter Type type;
 		private final String argument;
 
 		Event(Type type, String argument) {
@@ -270,9 +272,24 @@ public final class Workspace {
 			} 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,
+			/**
+			 * Somebody left a workspace
+			 * @see #getUserLeft() to get the name
+			 */
 			USER_LEAVE,
+			/**
+			 * The filetree was updated.
+			 * @see #getChangedBuffer() to see the buffer that changed
+			 */
 			FILE_TREE_UPDATED
 		}
 	}