2024-08-06 23:30:00 +02:00
|
|
|
package mp.code;
|
|
|
|
|
2024-08-07 10:22:01 +02:00
|
|
|
import java.util.Optional;
|
2024-08-19 11:36:51 +02:00
|
|
|
import java.util.UUID;
|
2024-10-03 03:07:14 +02:00
|
|
|
import java.util.function.Consumer;
|
2024-08-07 10:22:01 +02:00
|
|
|
|
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
|
|
|
}
|
|
|
|
|
|
|
|
private static native String get_workspace_id(long self);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Gets the unique identifier of the current workspace.
|
|
|
|
* @return the identifier
|
|
|
|
*/
|
2024-08-06 23:30:00 +02:00
|
|
|
public String getWorkspaceId() {
|
|
|
|
return get_workspace_id(this.ptr);
|
|
|
|
}
|
|
|
|
|
2024-08-07 10:22:01 +02:00
|
|
|
private static native CursorController get_cursor(long self);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Gets the {@link CursorController} for the current workspace.
|
|
|
|
* @return the {@link CursorController}
|
|
|
|
*/
|
2024-08-06 23:30:00 +02:00
|
|
|
public CursorController getCursor() {
|
2024-08-07 10:22:01 +02:00
|
|
|
return get_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-09-13 20:02:42 +02:00
|
|
|
private static native String[] get_file_tree(long self, String filter, boolean strict);
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Gets the file tree for this workspace, optionally filtering it.
|
|
|
|
* @param filter applies an optional filter to the outputs
|
|
|
|
* @param strict whether it should be a strict match (equals) or not (startsWith)
|
|
|
|
* @return an array containing file tree as flat paths
|
|
|
|
*/
|
|
|
|
@SuppressWarnings("OptionalUsedAsFieldOrParameterType")
|
2024-09-13 20:02:42 +02:00
|
|
|
public String[] getFileTree(Optional<String> filter, boolean strict) {
|
|
|
|
return get_file_tree(this.ptr, filter.orElse(null), strict);
|
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-09-25 17:36:20 +02:00
|
|
|
private static native String[] user_list(long self);
|
|
|
|
|
|
|
|
/**
|
|
|
|
* Returns the users currently in the workspace.
|
|
|
|
* @return an array containing the names of the users in the workspace
|
|
|
|
*/
|
|
|
|
public String[] userList() {
|
|
|
|
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-09-05 02:45:33 +02:00
|
|
|
private static native BufferController attach_to_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-09-05 02:45:33 +02:00
|
|
|
public BufferController attachToBuffer(String path) throws ConnectionException {
|
2024-09-17 23:16:39 +02:00
|
|
|
return attach_to_buffer(ptr, path);
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|
|
|
|
|
2024-09-26 02:29:46 +02:00
|
|
|
private static native boolean detach_from_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-09-26 02:29:46 +02:00
|
|
|
public boolean detachFromBuffer(String path) {
|
2024-09-17 23:16:39 +02:00
|
|
|
return detach_from_buffer(this.ptr, path);
|
2024-08-08 02:45:52 +02:00
|
|
|
}
|
|
|
|
|
2024-09-05 02:45:33 +02:00
|
|
|
private static native void fetch_buffers(long self) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Updates the local list of buffers.
|
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server
|
|
|
|
*/
|
2024-09-05 02:45:33 +02:00
|
|
|
public void fetchBuffers() throws ConnectionRemoteException {
|
2024-08-06 23:30:00 +02:00
|
|
|
fetch_buffers(this.ptr);
|
|
|
|
}
|
|
|
|
|
2024-09-05 02:45:33 +02:00
|
|
|
private static native void fetch_users(long self) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Updates the local list of users.
|
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server
|
|
|
|
*/
|
2024-09-05 02:45:33 +02:00
|
|
|
public void fetchUsers() throws ConnectionRemoteException {
|
2024-08-06 23:30:00 +02:00
|
|
|
fetch_buffers(this.ptr);
|
|
|
|
}
|
|
|
|
|
2024-09-05 02:45:33 +02:00
|
|
|
private static native UUID[] list_buffer_users(long self, String path) throws ConnectionRemoteException;
|
2024-09-17 23:16:39 +02:00
|
|
|
|
|
|
|
/**
|
|
|
|
* Lists the user attached to a certain buffer.
|
|
|
|
* The user must be attached to the buffer to perform this operation.
|
|
|
|
* @param path the path of the buffer to search
|
|
|
|
* @return an array of user {@link UUID UUIDs}
|
|
|
|
* @throws ConnectionRemoteException if an error occurs in communicating with the server, or the user wasn't attached
|
|
|
|
*/
|
2024-09-05 02:45:33 +02:00
|
|
|
public UUID[] listBufferUsers(String path) throws ConnectionRemoteException {
|
2024-09-17 23:16:39 +02:00
|
|
|
return list_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.
|
|
|
|
* @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-08-09 14:11:13 +02:00
|
|
|
private final Type type;
|
|
|
|
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-09-17 02:40:03 +02:00
|
|
|
enum Type {
|
2024-08-09 14:11:13 +02:00
|
|
|
USER_JOIN,
|
|
|
|
USER_LEAVE,
|
|
|
|
FILE_TREE_UPDATED
|
|
|
|
}
|
|
|
|
}
|
2024-08-06 23:30:00 +02:00
|
|
|
}
|