Skip to content

Commit

Permalink
custom initializationOptions
Browse files Browse the repository at this point in the history
  • Loading branch information
abentkamp committed Dec 14, 2023
1 parent 03fe278 commit b91645a
Showing 1 changed file with 6 additions and 2 deletions.
8 changes: 6 additions & 2 deletions client/src/editor/leanclient.ts
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,8 @@ export class LeanClient implements Disposable {

constructor (
private readonly connectionProvider: IConnectionProvider,
public readonly showRestartMessage: () => void) {
public readonly showRestartMessage: () => void,
private readonly initializationOptions = {}) {

}

Expand Down Expand Up @@ -106,8 +107,11 @@ export class LeanClient implements Disposable {
const clientOptions: LanguageClientOptions = {
// use a language id as a document selector
documentSelector: ['lean4'],
workspaceFolder: {uri: "hello"},
initializationOptions: {
editDelay: getElaborationDelay(), hasWidgets: true
editDelay: getElaborationDelay(),
hasWidgets: true,
...this.initializationOptions
},
connectionOptions: {
maxRestartCount: 0,
Expand Down

0 comments on commit b91645a

Please sign in to comment.