wip client

client/src/components/editor/Editor.tsx

@@ -11,7 +11,7 @@ import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
 import '../../css/editor.css'
 import { useSelector } from 'react-redux';
 import { selectTypewriterMode } from '../../state/progress';
-import { Typewriter } from './typewriter';
+import { Typewriter } from './Typewriter';
 import { GoalTabs } from './goal_tabs';
 import { GameInfoview } from './tmp';
 
@@ -24,7 +24,7 @@ export function Editor() {
   const editorRef = useRef<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(null)
   const gameInfoviewRef = useRef<HTMLDivElement>(null)
-  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor>()
+  const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|undefined>(undefined)
   const [leanMonaco, setLeanMonaco] = useState<LeanMonaco>()
   const [code, setCode] = useState<string>('')
 

client/src/components/editor/goal.tsx

@@ -1,8 +1,8 @@
 import * as React from 'react';
-import { InteractiveGoal, InteractiveHypothesisBundle } from '../Defs';
+import { InteractiveGoal, InteractiveHypothesisBundle } from './Defs';
 import { useTranslation } from 'react-i18next';
 import { InteractiveCode, InteractiveHypothesisBundle_nonAnonymousNames, LocationsContext, SubexprInfo, TaggedText } from '@leanprover/infoview';
-import { SelectableLocation } from '../../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
+// import { SelectableLocation } from '../../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {

client/src/components/editor/tmp.tsx

@@ -6,7 +6,7 @@ import type { DidCloseTextDocumentParams, DocumentUri, Location } from 'vscode-l
 import '@vscode/codicons/dist/codicon.css'
 import '@vscode/codicons/dist/codicon.ttf'
 import 'tachyons/css/tachyons.css'
-import './index.css'
+// import './index.css'
 
 import {
     defaultInfoviewConfig,