Class EditorConnection

Provides higher-level wrappers around functionality provided by the editor, e.g. to insert a comment. See also EditorApi.

Index

Constructors

Properties

Methods

copyToComment requestPlainGoal requestPlainTermGoal revealLocation revealPosition

Constructors

constructor

new EditorConnection(api: EditorApi, events: EditorEvents): EditorConnection
Parameters
- api: EditorApi
- events: EditorEvents
Returns EditorConnection
- Defined in lean4-infoview/src/infoview/editorConnection.ts:29

Properties

`Readonly`api

`Readonly`events

events: EditorEvents

Methods

copyToComment

copyToComment(text: string): Promise<void>
Copies the text to a comment at the cursor position.
Parameters
- text: string
Returns Promise<void>
- Defined in lean4-infoview/src/infoview/editorConnection.ts:55

requestPlainGoal

requestPlainGoal(pos: DocumentPosition): Promise<PlainGoal | undefined>
Parameters
- pos: DocumentPosition
Returns Promise<PlainGoal | undefined>
- Defined in lean4-infoview/src/infoview/editorConnection.ts:59

requestPlainTermGoal

requestPlainTermGoal(pos: DocumentPosition): Promise<PlainTermGoal | undefined>
Parameters
- pos: DocumentPosition
Returns Promise<PlainTermGoal | undefined>
- Defined in lean4-infoview/src/infoview/editorConnection.ts:64

revealLocation

revealLocation(loc: Location): Promise<void>
Highlights the given range in a document in the editor.
Parameters
- loc: Location
Returns Promise<void>
- Defined in lean4-infoview/src/infoview/editorConnection.ts:35

revealPosition

revealPosition(pos: DocumentPosition): Promise<void>
Parameters
- pos: DocumentPosition
Returns Promise<void>
- Defined in lean4-infoview/src/infoview/editorConnection.ts:43