WorkspaceAction

Actions about the workspace as a whole: creating/opening/closing/selecting pages, rather than editing an existing one's content.

Types

The user resolved a close-dirty-page prompt.

data class NewDocumentPage(val suggestedName: String? = null, val initialText: String = "") : WorkspaceAction

Creates a new page backed by a brand-new, not-yet-saved document.

data class NewPageForDocument(val documentId: DocumentId, val suggestedTitle: String? = null) : WorkspaceAction

Creates another page for an already-open document (so it can be edited/queried independently in parallel).

data class NewScratchPage(val suggestedTitle: String? = null, val initialText: String = "") : WorkspaceAction

Creates a new page backed by a page-local scratch buffer, never persisted as its own document.

data class OpenDocumentLoaded(val origin: DocumentOrigin, val text: String, val pending: Boolean = false) : WorkspaceAction

A document was read from an external source and should become a new page.

The user asked to close a page; if its document is dirty, a confirmation effect is requested first.

Asks the hosting platform to show an "open file" picker (see GuiEffect.PickOpenDocument).

Makes pageId the workspace's selected page.