more cleanup

client/src/Editor.tsx

@@ -15,6 +15,8 @@ import Split from 'react-split'
 import Notification from './Notification'
 import { monacoSetup } from './monacoSetup'
 import { config } from './config/config'
+import { IConnectionProvider } from 'monaco-languageclient'
+import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
 
 const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket"
 
@@ -65,8 +67,32 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string}> =
       new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
     }
 
+    const connectionProvider : IConnectionProvider = {
+      get: async () => {
+        return await new Promise((resolve, reject) => {
+          console.log(`connecting ${socketUrl}`)
+          const websocket = new WebSocket(socketUrl)
+          websocket.addEventListener('error', (ev) => {
+            reject(ev)
+          })
+          websocket.addEventListener('message', (msg) => {
+            // console.log(msg.data)
+          })
+          websocket.addEventListener('open', () => {
+            const socket = toSocket(websocket)
+            const reader = new WebSocketMessageReader(socket)
+            const writer = new WebSocketMessageWriter(socket)
+            resolve({
+              reader,
+              writer
+            })
+          })
+        })
+      }
+    }
+
     // Following `vscode-lean4/webview/index.ts`
-    const client = new LeanClient(socketUrl, undefined, uri, showRestartMessage)
+    const client = new LeanClient(connectionProvider, showRestartMessage)
     const infoProvider = new InfoProvider(client)
     const div: HTMLElement = infoviewRef.current!
     const imports = {

client/src/editor/infoview.ts

@@ -51,8 +51,6 @@ export class InfoProvider implements Disposable {
   private readonly subscriptions: Disposable[] = []
   private readonly clientSubscriptions: Disposable[] = []
 
-  private readonly stylesheet: string = ''
-  private readonly autoOpened: boolean = false
   public readonly client?: LeanClient
   // private readonly clientProvider: LeanClientProvider
 
@@ -62,9 +60,6 @@ export class InfoProvider implements Disposable {
 
   private rpcSessions: Map<string, RpcSessionAtPos> = new Map()
 
-  // the key is the LeanClient.getWorkspaceFolder()
-  private readonly clientsFailed: Map<string, any> = new Map()
-
   // the key is the uri of the file who's worker has failed.
   private readonly workersFailed: Map<string, any> = new Map()
 
@@ -201,8 +196,7 @@ export class InfoProvider implements Disposable {
       }
     },
     copyToClipboard: async (text) => {
-      await window.clipboard.writeText(text)
-      await window.showInformationMessage(`Copied to clipboard: ${text}`)
+      navigator.clipboard.writeText(text)
     },
     insertText: async (text, kind, tdpp) => {
       let uri: Uri | undefined
@@ -488,29 +482,19 @@ export class InfoProvider implements Disposable {
     const editor = this.editor
     if (editor == null) return
     const loc = this.getLocation(editor)
-    // if (languages.match(this.leanDocs, editor.document) === 0) {
-    //   // language is not yet 'lean4', but the LeanClient will fire the didSetLanguage event
-    //   // in openLean4Document and that's when we can send the position to update the
-    //   // InfoView for the newly opened document.
-    //   return
-    // }
-    // actual editor
-    if (this.clientsFailed.size > 0 || this.workersFailed.size > 0) {
-      const client = this.client // this.clientProvider.findClient(editor.document.uri.toString())
-      if (client != null) {
-        const uri = window.activeTextEditor?.document.uri.toString() ?? ''
-        let reason: any | undefined
-        if (this.workersFailed.has(uri)) {
-          reason = this.workersFailed.get(uri)
-        }
-        if (reason) {
-          // send stopped event
-          await this.infoviewApi?.serverStopped(reason)
-        } else {
-          await this.updateStatus(loc)
-        }
+    if (!this.client.running){
+      await this.infoviewApi?.serverStopped(undefined)
+    } else if (this.workersFailed.size > 0) {
+      const uri = window.activeTextEditor?.document.uri.toString() ?? ''
+      let reason: any | undefined
+      if (this.workersFailed.has(uri)) {
+        reason = this.workersFailed.get(uri)
+      }
+      if (reason) {
+        // send stopped event
+        await this.infoviewApi?.serverStopped(reason)
       } else {
-        console.log('[InfoProvider] ### what does it mean to have sendPosition but no LeanClient for this document???')
+        await this.updateStatus(loc)
       }
     } else {
       await this.updateStatus(loc)

client/src/editor/leanclient.ts

@@ -3,8 +3,8 @@
 import {
   TextDocument, EventEmitter, Diagnostic,
   DocumentHighlight, Range, DocumentHighlightKind,
-  Disposable, Uri, ConfigurationChangeEvent, DiagnosticCollection,
-  WorkspaceFolder, window
+  Disposable, Uri, DiagnosticCollection,
+  WorkspaceFolder
 } from 'vscode'
 import {
   DidChangeTextDocumentParams,
@@ -13,11 +13,10 @@ import {
   MonacoLanguageClient as LanguageClient,
   LanguageClientOptions,
   PublishDiagnosticsParams,
-  CloseAction, ErrorAction,
+  CloseAction, ErrorAction, IConnectionProvider,
 } from 'monaco-languageclient'
 import { State } from 'vscode-languageclient'
 import * as ls from 'vscode-languageserver-protocol'
-import { toSocket, WebSocketMessageReader, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
 
 import { getElaborationDelay } from './config'
 import { LeanFileProgressParams, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'
@@ -76,9 +75,10 @@ export class LeanClient implements Disposable {
   /** Files which are open. */
   private readonly isOpen: Map<string, TextDocument> = new Map()
 
-  constructor (private readonly socketUrl: string, workspaceFolder: WorkspaceFolder | undefined, folderUri: Uri,
+  constructor (
+    private readonly connectionProvider: IConnectionProvider,
     public readonly showRestartMessage: () => void) {
-    this.folderUri = folderUri
+
   }
 
   dispose (): void {
@@ -189,29 +189,7 @@ export class LeanClient implements Disposable {
         id: 'lean4',
         name: 'Lean 4',
         clientOptions,
-        connectionProvider: {
-          get: async () => {
-            return await new Promise((resolve, reject) => {
-              console.log(`connecting ${this.socketUrl}`)
-              const websocket = new WebSocket(this.socketUrl)
-              websocket.addEventListener('error', (ev) => {
-                reject(ev)
-              })
-              websocket.addEventListener('message', (msg) => {
-                // console.log(msg.data)
-              })
-              websocket.addEventListener('open', () => {
-                const socket = toSocket(websocket)
-                const reader = new WebSocketMessageReader(socket)
-                const writer = new WebSocketMessageWriter(socket)
-                resolve({
-                  reader,
-                  writer
-                })
-              })
-            })
-          }
-        }
+        connectionProvider: this.connectionProvider
       })
     } else {
       await this.client.start()