work on client

leanprover-community · Feb 26, 2025 · c199947 · c199947
1 parent 0173688
commit c199947
Show file tree

Hide file tree

Showing 4 changed files with 143 additions and 465 deletions.
diff --git a/client/src/components/editor/Editor.tsx b/client/src/components/editor/Editor.tsx
@@ -11,7 +11,8 @@ import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
 import '../../css/editor.css'
 import { useSelector } from 'react-redux';
 import { selectTypewriterMode } from '../../state/progress';
-// import { TypewriterInterFace } from './Typewriter';
+import { Typewriter } from './typewriter';
+import { GoalTabs } from './infoview/goal_tabs';
 
 export function Editor() {
   let { t } = useTranslation()
@@ -98,7 +99,7 @@ export function Editor() {
         <div ref={editorRef} id="editor" />
         <div ref={infoviewRef} id="infoview" />
       </Split>
-      {/* {typewriterMode && <TypewriterInterFace />} */}
+      {editor && typewriterMode && <Typewriter />}
     </div>
   </MonacoEditorContext.Provider>
 }