2024-08-06 23:30:00 +02:00
|
|
|
package mp.code;
|
|
|
|
|
2024-08-07 10:22:01 +02:00
|
|
|
import java.util.Optional;
|
2024-10-03 03:07:14 +02:00
|
|
|
import java.util.function.Consumer;
|
2024-08-07 10:22:01 +02:00
|
|
|
|
2024-10-15 22:36:43 +02:00
|
|
|
import lombok.Getter;
|
2024-10-16 00:42:55 +02:00
|
|
|
import mp.code.data.User;
|
2024-09-05 02:45:33 +02:00
|
|
|
import mp.code.exceptions.ConnectionException;
|
|
|
|
import mp.code.exceptions.ConnectionRemoteException;
|
|
|
|
import mp.code.exceptions.ControllerException;
|
2024-08-06 23:30:00 +02:00
|
|
|
|
2024-09-17 23:16:39 +02:00
|
|
|
/**
|
|
|
|
* Represents a CodeMP workspace, which broadly speaking is a collection
|
|
|
|
* of buffers across which edits and cursor movements are tracked.
|
2024-09-18 03:27:33 +02:00
|
|
|
* Generally, it is safer to avoid storing this directly. Instead,
|
|
|
|
* users should let the native library manage as much as possible for
|
|
|
|
* them. They should store the workspace ID and retrieve the object
|
|
|
|
* whenever needed with {@link Client#getWorkspace(String)}.
|
2024-09-17 23:16:39 +02:00
|
|
|
*/
|
|
|
|
public final class Workspace {
|
2024-08-06 23:30:00 +02:00
|
|
|
private final long ptr;
|
|
|
|
|
|
|
|
Workspace(long ptr) {
|
|
|
|
this.ptr = ptr;
|
2024-09-18 15:36:11 +02:00
|
|
|
Extensions.CLEANER.register(this, () -> free(ptr));
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-15 23:01:49 +02:00
|
|
|
private static native String id(long self);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Gets the unique identifier of the current workspace.
|
|
|
|
* @return the identifier
|
|
|
|
*/
|
2024-10-15 23:01:49 +02:00
|
|
|
public String id() {
|
|
|
|
return id(this.ptr);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-15 23:01:49 +02:00
|
|
|
private static native CursorController cursor(long self);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Gets the {@link CursorController} for the current workspace.
|
|
|
|
* @return the {@link CursorController}
|
|
|
|
*/
|
2024-10-15 23:01:49 +02:00
|
|
|
public CursorController cursor() {
|
|
|
|
return cursor(this.ptr);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-08-07 10:22:01 +02:00
|
|
|
private static native BufferController get_buffer(long self, String path);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Looks for a {@link BufferController} with the given path within the
|
|
|
|
* current workspace and returns it if it exists.
|
|
|
|
* @param path the current path
|
|
|
|
* @return the {@link BufferController} with the given path, if it exists
|
|
|
|
*/
|
2024-08-07 10:22:01 +02:00
|
|
|
public Optional<BufferController> getBuffer(String path) {
|
2024-09-17 23:16:39 +02:00
|
|
|
return Optional.ofNullable(get_buffer(this.ptr, path));
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-16 00:42:55 +02:00
|
|
|
private static native String[] search_buffers(long self, String filter);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
2024-10-16 00:42:55 +02:00
|
|
|
* Searches for buffers matching the filter in this workspace.
|
|
|
|
* @param filter the filter to apply
|
2024-09-17 23:16:39 +02:00
|
|
|
* @return an array containing file tree as flat paths
|
|
|
|
*/
|
|
|
|
@SuppressWarnings("OptionalUsedAsFieldOrParameterType")
|
2024-10-16 00:42:55 +02:00
|
|
|
public String[] searchBuffers(Optional<String> filter) {
|
|
|
|
return search_buffers(this.ptr, filter.orElse(null));
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-09-17 02:40:03 +02:00
|
|
|
private static native String[] active_buffers(long self);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Returns the currently active buffers (the ones the user is currently
|
|
|
|
* attached to).
|
|
|
|
* @return an array containing the paths of the active buffers
|
|
|
|
*/
|
2024-09-17 02:40:03 +02:00
|
|
|
public String[] activeBuffers() {
|
|
|
|
return active_buffers(this.ptr);
|
|
|
|
}
|
|
|
|
|
2024-10-18 12:17:41 +02:00
|
|
|
private static native User[] user_list(long self);
|
2024-09-25 17:36:20 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Returns the users currently in the workspace.
|
2024-10-18 12:17:41 +02:00
|
|
|
* @return an array containing the users in the workspace
|
2024-09-25 17:36:20 +02:00
|
|
|
*/
|
2024-10-18 12:17:41 +02:00
|
|
|
public User[] userList() {
|
2024-09-25 17:36:20 +02:00
|
|
|
return user_list(this.ptr);
|
|
|
|
}
|
|
|
|
|
2024-09-17 02:40:03 +02:00
|
|
|
private static native void create_buffer(long self, String path) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Creates a buffer with the given path.
|
|
|
|
* @param path the new buffer's path
|
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server
|
|
|
|
*/
|
2024-09-05 02:45:33 +02:00
|
|
|
public void createBuffer(String path) throws ConnectionRemoteException {
|
2024-09-17 23:16:39 +02:00
|
|
|
create_buffer(this.ptr, path);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-15 23:01:49 +02:00
|
|
|
private static native BufferController attach_buffer(long self, String path) throws ConnectionException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Attaches to an existing buffer with the given path, if present.
|
|
|
|
* @param path the path of the buffer to attach to
|
|
|
|
* @return the {@link BufferController} associated with that path
|
|
|
|
* @throws ConnectionException if an error occurs in communicating with the server, or if the buffer did not exist
|
|
|
|
*/
|
2024-10-15 23:01:49 +02:00
|
|
|
public BufferController attachBuffer(String path) throws ConnectionException {
|
|
|
|
return attach_buffer(ptr, path);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-15 23:01:49 +02:00
|
|
|
private static native boolean detach_buffer(long self, String path);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Detaches from a given buffer.
|
|
|
|
* @param path the path of the buffer to detach from
|
2024-09-26 02:29:46 +02:00
|
|
|
* @return a boolean, true only if there are still dangling references preventing controller from stopping
|
2024-09-17 23:16:39 +02:00
|
|
|
*/
|
2024-10-15 23:01:49 +02:00
|
|
|
public boolean detachBuffer(String path) {
|
|
|
|
return detach_buffer(this.ptr, path);
|
2024-08-08 02:45:52 +02:00
|
|
|
}
|
|
|
|
|
2024-10-16 00:42:55 +02:00
|
|
|
private static native String[] fetch_buffers(long self) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
2024-10-16 00:42:55 +02:00
|
|
|
* Updates and fetches the local list of buffers.
|
|
|
|
* @return the updated list
|
2024-09-17 23:16:39 +02:00
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server
|
|
|
|
*/
|
2024-10-16 00:42:55 +02:00
|
|
|
public String[] fetchBuffers() throws ConnectionRemoteException {
|
|
|
|
return fetch_buffers(this.ptr);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-16 00:42:55 +02:00
|
|
|
private static native User[] fetch_users(long self) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
2024-10-16 00:42:55 +02:00
|
|
|
* Updates and fetches the local list of users.
|
|
|
|
* @return the updated list
|
2024-09-17 23:16:39 +02:00
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server
|
|
|
|
*/
|
2024-10-16 00:42:55 +02:00
|
|
|
public User[] fetchUsers() throws ConnectionRemoteException {
|
|
|
|
return fetch_users(this.ptr);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-16 00:42:55 +02:00
|
|
|
private static native User[] fetch_buffer_users(long self, String path) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
2024-10-16 00:42:55 +02:00
|
|
|
* Fetches the users attached to a certain buffer.
|
2024-09-17 23:16:39 +02:00
|
|
|
* The user must be attached to the buffer to perform this operation.
|
|
|
|
* @param path the path of the buffer to search
|
2024-10-16 00:42:55 +02:00
|
|
|
* @return an array of {@link User}s
|
2024-09-17 23:16:39 +02:00
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server, or the user wasn't attached
|
|
|
|
*/
|
2024-10-16 00:42:55 +02:00
|
|
|
public User[] fetchBufferUsers(String path) throws ConnectionRemoteException {
|
|
|
|
return fetch_buffer_users(this.ptr, path);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-09-05 02:45:33 +02:00
|
|
|
private static native void delete_buffer(long self, String path) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Deletes the buffer with the given path.
|
|
|
|
* @param path the path of the buffer to delete
|
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server
|
|
|
|
*/
|
2024-09-05 02:45:33 +02:00
|
|
|
public void deleteBuffer(String path) throws ConnectionRemoteException {
|
2024-09-17 23:16:39 +02:00
|
|
|
delete_buffer(this.ptr, path);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-10-03 03:07:14 +02:00
|
|
|
private static native Event try_recv(long self) throws ControllerException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
2024-10-03 03:07:14 +02:00
|
|
|
* Tries to get a {@link Event} from the queue if any were present, and returns
|
|
|
|
* an empty optional otherwise.
|
|
|
|
* @return the first workspace event in queue, if any are present
|
|
|
|
* @throws ControllerException if the controller was stopped
|
2024-09-17 23:16:39 +02:00
|
|
|
*/
|
2024-10-03 03:07:14 +02:00
|
|
|
public Optional<Event> tryRecv() throws ControllerException {
|
|
|
|
return Optional.ofNullable(try_recv(this.ptr));
|
|
|
|
}
|
|
|
|
|
|
|
|
private static native Event recv(long self) throws ControllerException;
|
|
|
|
|
|
|
|
/**
|
|
|
|
* Blocks until a {@link Event} is available and returns it.
|
|
|
|
* @return the workspace event that occurred
|
|
|
|
* @throws ControllerException if the controller was stopped
|
|
|
|
*/
|
|
|
|
public Event recv() throws ControllerException {
|
|
|
|
return recv(this.ptr);
|
|
|
|
}
|
|
|
|
|
|
|
|
private static native void callback(long self, Consumer<Workspace> cb);
|
|
|
|
|
|
|
|
/**
|
|
|
|
* Registers a callback to be invoked whenever a new {@link Event} is ready to be received.
|
|
|
|
* This will not work unless a Java thread has been dedicated to the event loop.
|
2024-10-15 21:55:23 +02:00
|
|
|
* @param cb a {@link Consumer} that receives the controller when the change occurs;
|
|
|
|
* you should probably spawn a new thread in here, to avoid deadlocking
|
2024-10-03 03:07:14 +02:00
|
|
|
* @see Extensions#drive(boolean)
|
|
|
|
*/
|
|
|
|
public void callback(Consumer<Workspace> cb) {
|
|
|
|
callback(this.ptr, cb);
|
|
|
|
}
|
|
|
|
|
|
|
|
private static native void clear_callback(long self);
|
|
|
|
|
|
|
|
/**
|
|
|
|
* Clears the registered callback.
|
|
|
|
* @see #callback(Consumer)
|
|
|
|
*/
|
|
|
|
public void clearCallback() {
|
|
|
|
clear_callback(this.ptr);
|
|
|
|
}
|
|
|
|
|
|
|
|
private static native void poll(long self) throws ControllerException;
|
|
|
|
|
|
|
|
/**
|
|
|
|
* Blocks until a {@link Event} is available.
|
|
|
|
* @throws ControllerException if the controller was stopped
|
|
|
|
*/
|
|
|
|
public void poll() throws ControllerException {
|
|
|
|
poll(this.ptr);
|
2024-08-09 14:11:13 +02:00
|
|
|
}
|
|
|
|
|
2024-08-06 23:30:00 +02:00
|
|
|
private static native void free(long self);
|
2024-09-17 02:40:03 +02:00
|
|
|
|
|
|
|
static {
|
2024-09-18 14:54:54 +02:00
|
|
|
NativeUtils.loadLibraryIfNeeded();
|
2024-09-17 02:40:03 +02:00
|
|
|
}
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Represents a workspace-wide event.
|
|
|
|
*/
|
|
|
|
public static final class Event {
|
2024-10-15 22:36:43 +02:00
|
|
|
/** The type of the event. */
|
|
|
|
public final @Getter Type type;
|
2024-08-09 14:11:13 +02:00
|
|
|
private final String argument;
|
|
|
|
|
|
|
|
Event(Type type, String argument) {
|
|
|
|
this.type = type;
|
|
|
|
this.argument = argument;
|
|
|
|
}
|
|
|
|
|
2024-09-17 23:16:39 +02:00
|
|
|
/**
|
|
|
|
* Gets the user who joined, if any did.
|
|
|
|
* @return the user who joined, if any did
|
|
|
|
*/
|
2024-09-16 00:20:03 +02:00
|
|
|
public Optional<String> getUserJoined() {
|
2024-08-09 14:11:13 +02:00
|
|
|
if(this.type == Type.USER_JOIN) {
|
|
|
|
return Optional.of(this.argument);
|
|
|
|
} else return Optional.empty();
|
|
|
|
}
|
|
|
|
|
2024-09-17 23:16:39 +02:00
|
|
|
/**
|
|
|
|
* Gets the user who left, if any did.
|
|
|
|
* @return the user who left, if any did
|
|
|
|
*/
|
2024-08-09 14:11:13 +02:00
|
|
|
public Optional<String> getUserLeft() {
|
|
|
|
if(this.type == Type.USER_LEAVE) {
|
|
|
|
return Optional.of(this.argument);
|
|
|
|
} else return Optional.empty();
|
|
|
|
}
|
|
|
|
|
2024-09-17 23:16:39 +02:00
|
|
|
/**
|
|
|
|
* Gets the path of buffer that changed, if any did.
|
|
|
|
* @return the path of buffer that changed, if any did
|
|
|
|
*/
|
|
|
|
public Optional<String> getChangedBuffer() {
|
2024-08-19 11:36:51 +02:00
|
|
|
if(this.type == Type.FILE_TREE_UPDATED) {
|
|
|
|
return Optional.of(this.argument);
|
|
|
|
} else return Optional.empty();
|
2024-08-09 14:11:13 +02:00
|
|
|
}
|
|
|
|
|
2024-10-15 22:36:43 +02:00
|
|
|
/**
|
|
|
|
* The type of workspace event.
|
|
|
|
*/
|
|
|
|
public enum Type {
|
|
|
|
/**
|
|
|
|
* Somebody joined a workspace.
|
|
|
|
* @see #getUserJoined() to get the name
|
|
|
|
*/
|
2024-08-09 14:11:13 +02:00
|
|
|
USER_JOIN,
|
2024-10-15 22:36:43 +02:00
|
|
|
/**
|
|
|
|
* Somebody left a workspace
|
|
|
|
* @see #getUserLeft() to get the name
|
|
|
|
*/
|
2024-08-09 14:11:13 +02:00
|
|
|
USER_LEAVE,
|
2024-10-15 22:36:43 +02:00
|
|
|
/**
|
|
|
|
* The filetree was updated.
|
|
|
|
* @see #getChangedBuffer() to see the buffer that changed
|
|
|
|
*/
|
2024-08-09 14:11:13 +02:00
|
|
|
FILE_TREE_UPDATED
|
|
|
|
}
|
|
|
|
}
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|