style

Author: joneugster

Diff for: cypress/e2e/spec.cy.ts

@@ -2,7 +2,7 @@ describe('Editor Test', () => {
   it('displays the editor', () => {
     cy.visit('http://localhost:5173/')
     cy.contains('#check 0')
-      .should(($p) => {
+      .should(($p: any) => {
         // ...
         expect(getComputedStyle($p.get(0)).fontFamily).to.match(/^JuliaMono/)
       })
@@ -18,12 +18,12 @@ describe('Editor Test', () => {
     cy.visit('http://localhost:5173/')
     cy.get('[data-cy="theme-light"]').click()
     cy.contains('#check 0')
-      .should(($p) => {
+      .should(($p: any) => {
         expect(getComputedStyle($p.get(0)).getPropertyValue('--vscode-editor-background')).to.equal("#ffffff")
       })
     cy.get('[data-cy="theme-dark"]').click()
     cy.contains('#check 0')
-      .should(($p) => {
+      .should(($p: any) => {
         expect(getComputedStyle($p.get(0)).getPropertyValue('--vscode-editor-background')).to.equal("#1e1e1e")
       })
 

Diff for: demo/src/App.css

@@ -3,8 +3,6 @@
   height: 300px;
 }
 
-
 .controls {
   flex: 0 0 100%;
 }
-

Diff for: demo/src/App.tsx

@@ -1,16 +1,26 @@
 import { useState } from 'react'
-import './App.css'
 import LeanMonacoComponent from './LeanMonaco'
 import { LeanMonacoOptions } from 'lean4monaco'
+import './App.css'
 
 function App() {
-  const [options, setOptions] = useState<LeanMonacoOptions>({websocket: {url: 'ws://localhost:8080/'}, vscode: {
-    "workbench.colorTheme": "Visual Studio Light",
-    /* To add settings here, you can open your settings in VSCode (Ctrl+,), search
-     * for the desired setting, select "Copy Setting as JSON" from the "More Actions"
-     * menu next to the selected setting, and paste the copied string here.
-     */
-  }})
+
+  /* lean-Monaco options. The websocket URL is where the server should listen.
+   * To add settings in `vscode` (i.e. for the editor),
+   * you can open your settings in VSCode (Ctrl+,), search
+   * for the desired setting, select "Copy Setting as JSON" from the "More Actions"
+   * menu next to the selected setting, and paste the copied string here.
+   */
+  const [options, setOptions] = useState<LeanMonacoOptions>({
+    websocket: {
+      url: 'ws://localhost:8080/'
+    },
+    vscode: {
+      "workbench.colorTheme": "Visual Studio Light",
+    }
+  })
+
+  // state to keep track of the number of open editors
   const [numberEditors, setNumberEditors] = useState(1)
 
   return (

Diff for: demo/src/LeanMonaco.tsx

@@ -1,31 +1,32 @@
 import { useEffect, useRef, createContext, useState } from 'react'
 import { LeanMonaco, LeanMonacoOptions } from 'lean4monaco'
-import LeanMonacoEditorComponent from './LeanMonacoEditor';
+import LeanMonacoEditorComponent from './LeanMonacoEditor'
 
 export const LeanMonacoContext = createContext<LeanMonaco|null>(null);
 
 function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOptions, numberEditors: number}) {
   const [leanMonaco, setLeanMonaco] = useState<LeanMonaco|null>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
 
+  // You need to start one `LeanMonaco` instance once in your application using a `useEffect`
   useEffect(() => {
     const leanMonaco = new LeanMonaco()
     setLeanMonaco(leanMonaco)
     leanMonaco.setInfoviewElement(infoviewRef.current!)
-    
+
     ;(async () => {
-        await leanMonaco.start(options)
+      await leanMonaco.start(options)
     })()
-    
+
     return () => {
-        leanMonaco.dispose()
+      leanMonaco.dispose()
     }
   }, [options])
 
   return (
     <>
       <LeanMonacoContext.Provider value={leanMonaco}>
-        {[...Array(numberEditors)].map((x, i) =>
+        {[...Array(numberEditors)].map((_x, i) =>
           <LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`} value={`#check ${i}`}/>
         )}
         <div className='infoview' ref={infoviewRef}></div>

Diff for: demo/src/LeanMonacoEditor.tsx

@@ -6,23 +6,24 @@ function LeanMonacoEditorComponent({fileName, value}: {fileName: string, value:
   const codeviewRef = useRef<HTMLDivElement>(null)
   const leanMonaco = useContext(LeanMonacoContext)
 
+  // You can start multiple `LeanMonacoEditor` instances
   useEffect(() => {
     if (leanMonaco) {
       const leanMonacoEditor = new LeanMonacoEditor()
-      
+
       ;(async () => {
-          await leanMonaco!.whenReady
-          await leanMonacoEditor.start(codeviewRef.current!, fileName, value)
+        await leanMonaco!.whenReady
+        await leanMonacoEditor.start(codeviewRef.current!, fileName, value)
       })()
-      
+
       return () => {
-          leanMonacoEditor.dispose()
+        leanMonacoEditor.dispose()
       }
     }
   }, [leanMonaco])
 
   return (
-      <div className='codeview' ref={codeviewRef}></div>
+    <div className='codeview' ref={codeviewRef}></div>
   )
 }
 

Diff for: demo/src/index.css

@@ -25,6 +25,7 @@ a {
   color: #646cff;
   text-decoration: inherit;
 }
+
 a:hover {
   color: #535bf2;
 }
@@ -52,11 +53,12 @@ button {
   cursor: pointer;
   transition: border-color 0.25s;
 }
+
 button:hover {
   border-color: #646cff;
 }
-button:focus,
-button:focus-visible {
+
+button:focus, button:focus-visible {
   outline: 4px auto -webkit-focus-ring-color;
 }
 
@@ -65,9 +67,11 @@ button:focus-visible {
     color: #213547;
     background-color: #ffffff;
   }
+
   a:hover {
     color: #747bff;
   }
+
   button {
     background-color: #f9f9f9;
   }

Diff for: demo/src/main.tsx

@@ -6,5 +6,5 @@ import './index.css'
 ReactDOM.createRoot(document.getElementById('root')!).render(
   <React.StrictMode>
     <App />
-  </React.StrictMode>,
+  </React.StrictMode>
 )

Diff for: demo/src/vite-env.d.ts

@@ -25,15 +25,17 @@ export default defineConfig({
         {
           src: [
             normalizePath(path.resolve(__dirname, '../node_modules/@leanprover/infoview/dist/*')),
+            // note: if you install `lean4monaco` via npm, this line need to change, see README.
             normalizePath(path.resolve(__dirname, '../dist/webview/webview.js')),
           ],
           dest: 'infoview'
         }
       ]
-    }) as PluginOption
+    })
   ],
   server: {
     fs: {
+      // only needed because `demo` lies inside the `lean4monaco` folder
       allow: [".."]
     }
   },

Diff for: demo/vite.config.ts

@@ -1,8 +1,8 @@
-import { Uri } from 'vscode';
-import { fs } from 'memfs';
-import { ITextFileEditorModel, createModelReference } from 'vscode/monaco';
-import * as monaco from 'monaco-editor';
-import { IReference } from '@codingame/monaco-vscode-editor-service-override';
+import { Uri } from 'vscode'
+import { fs } from 'memfs'
+import { ITextFileEditorModel, createModelReference } from 'vscode/monaco'
+import * as monaco from 'monaco-editor'
+import { IReference } from '@codingame/monaco-vscode-editor-service-override'
 import path from 'path'
 
 export class LeanMonacoEditor {
@@ -15,12 +15,12 @@ export class LeanMonacoEditor {
     if (this.disposed) return
 
     // Create file for clientProvider to find
-    fs.mkdirSync(path.dirname(fileName), {recursive: true});
-    fs.writeFileSync(fileName, '');
-    
+    fs.mkdirSync(path.dirname(fileName), {recursive: true})
+    fs.writeFileSync(fileName, '')
+
     // Create editor and model
-    this.modelRef = await createModelReference(Uri.parse(fileName), code);
-    this.editor = monaco.editor.create(editorEl, { automaticLayout: true });
+    this.modelRef = await createModelReference(Uri.parse(fileName), code)
+    this.editor = monaco.editor.create(editorEl, { automaticLayout: true })
     this.editor.setModel(this.modelRef.object.textEditorModel)
 
     // Set focus on editor to trigger infoview to open