test multiple editors

Author: abentkamp

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

@@ -1,40 +1,55 @@
 describe('Editor Test', () => {
   it('displays the editor', () => {
     cy.visit('http://localhost:5173/')
-    cy.contains('#check Nat')
+    cy.contains('#check 0')
       .should(($p) => {
         // ...
         expect(getComputedStyle($p.get(0)).fontFamily).to.match(/^JuliaMono/)
       })
   })
+
   it('displays the infoview', () => {
     cy.visit('http://localhost:5173/')
     cy.get('.squiggly-info')
-    cy.iframe().contains('Nat : Type')
+    cy.iframe().contains('0 : Nat')
   })
-  it('changes themes', () => {
 
+  it('changes themes', () => {
     cy.visit('http://localhost:5173/')
     cy.get('[data-cy="theme-light"]').click()
-    cy.contains('#check Nat')
+    cy.contains('#check 0')
       .should(($p) => {
         expect(getComputedStyle($p.get(0)).getPropertyValue('--vscode-editor-background')).to.equal("#ffffff")
       })
     cy.get('[data-cy="theme-dark"]').click()
-    cy.contains('#check Nat')
+    cy.contains('#check 0')
       .should(($p) => {
         expect(getComputedStyle($p.get(0)).getPropertyValue('--vscode-editor-background')).to.equal("#1e1e1e")
       })
   })
+  
   it('inputs unicode', () => {
     cy.visit('http://localhost:5173/')
     cy.get('[data-cy="leader-backslash"]').click()
-    cy.contains('#check Nat').click("left")
+    cy.contains('#check 0').click("left")
     cy.get('body').type('\\alpha')
     cy.contains('α')
     cy.get('[data-cy="leader-comma"]').click()
-    cy.contains('#check Nat').click("left")
+    cy.contains('α#check 0').click("left")
     cy.get('body').type(',beta')
-    cy.contains('β')
+    cy.contains('βα#check 0')
+  })
+
+  it('allows for multiple editors', () => {
+    cy.visit('http://localhost:5173/')
+    cy.contains('#check 0')
+    cy.get('[data-cy="number-editors"]').type('{selectall}').type('2')
+    cy.contains('#check 1')
+    cy.contains('#check 0')
+    cy.get('.squiggly-info')
+    cy.contains('#check 1').click()
+    cy.iframe().contains('1 : Nat')
+    cy.contains('#check 0').click()
+    cy.iframe().contains('0 : Nat')
   })
 })

Diff for: demo/src/App.tsx

@@ -28,6 +28,7 @@ function App() {
         >Input Leader ","</button>
         <input type="number" min="1" max="3"
           value={numberEditors}
+          data-cy="number-editors"
           onChange={(event) => {
             setNumberEditors(parseInt(event.target.value));
           }}

Diff for: demo/src/LeanMonaco.tsx

@@ -26,7 +26,7 @@ function LeanMonacoComponent({options, numberEditors} : {options: LeanMonacoOpti
     <>
       <LeanMonacoContext.Provider value={leanMonaco}>
         {[...Array(numberEditors)].map((x, i) =>
-          <LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`}/>
+          <LeanMonacoEditorComponent key={i} fileName={`/project/test${i}.lean`} value={`#check ${i}`}/>
         )}
         <div className='infoview' ref={infoviewRef}></div>
       </LeanMonacoContext.Provider>

Diff for: demo/src/LeanMonacoEditor.tsx

@@ -2,7 +2,7 @@ import { useEffect, useRef, useContext } from 'react'
 import { LeanMonacoEditor } from 'lean4monaco'
 import { LeanMonacoContext } from './LeanMonaco'
 
-function LeanMonacoEditorComponent({fileName}: {fileName: string}) {
+function LeanMonacoEditorComponent({fileName, value}: {fileName: string, value: string}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const leanMonaco = useContext(LeanMonacoContext)
 
@@ -12,7 +12,7 @@ function LeanMonacoEditorComponent({fileName}: {fileName: string}) {
 
       ;(async () => {
           await leanMonaco!.whenReady
-          await leanMonacoEditor.start(codeviewRef.current!, fileName, '#check Nat')
+          await leanMonacoEditor.start(codeviewRef.current!, fileName, value)
       })()
 
       return () => {