wip

client/src/components/infoview/rpc_api.ts → client/src/components/editor/Defs.ts

@@ -1,67 +1,72 @@
 /**
  *  @fileOverview Defines the interface for the communication with the server.
  *
- * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
  */
-import type { Range } from 'vscode-languageserver-protocol';
-// import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
-// import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
-import type { Diagnostic } from 'vscode-languageserver-protocol';
+import type { Range } from 'vscode-languageserver-protocol'
+import type {
+  CodeWithInfos,
+  ContextInfo,
+  FVarId,
+  InteractiveDiagnostic,
+  MVarId,
+  TermInfo
+} from '@leanprover/infoview-api'
+import type { Diagnostic } from 'vscode-languageserver-protocol'
 
 export interface InteractiveHypothesisBundle {
   /** The pretty names of the variables in the bundle. Anonymous names are rendered
    * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
    * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
-  names: string[];
-  fvarIds?: any // FVarId[];
-  type: any // CodeWithInfos;
-  val?: any // CodeWithInfos;
-  isInstance?: boolean;
-  isType?: boolean;
-  isInserted?: boolean;
-  isRemoved?: boolean;
-  isAssumption?: boolean;
+  names: string[]
+  fvarIds?: FVarId[]
+  type: CodeWithInfos
+  val?: CodeWithInfos
+  isInstance?: boolean
+  isType?: boolean
+  isInserted?: boolean
+  isRemoved?: boolean
+  isAssumption?: boolean
 }
 
 export interface InteractiveGoalCore {
-  hyps: InteractiveHypothesisBundle[];
-  type: any // CodeWithInfos;
-  ctx?: any // ContextInfo;
+  hyps: InteractiveHypothesisBundle[]
+  type: CodeWithInfos
+  ctx?: ContextInfo
 }
 
 export interface InteractiveGoal extends InteractiveGoalCore {
-  userName?: string;
-  goalPrefix?: string;
-  mvarId?: any // MVarId;
-  isInserted?: boolean;
-  isRemoved?: boolean;
+  userName?: string
+  goalPrefix?: string
+  mvarId?: MVarId
+  isInserted?: boolean
+  isRemoved?: boolean
 }
 
 export interface InteractiveGoals extends InteractiveGoalCore {
-  goals: InteractiveGoals[];
+  goals: InteractiveGoals[]
 }
 
 export interface InteractiveTermGoal extends InteractiveGoalCore {
-  range?: Range;
-  term?: any //TermInfo;
+  range?: Range
+  term?: TermInfo
 }
 
 export interface GameHint {
-  text: string;
-  hidden: boolean;
-  rawText: string;
-  varNames?: string[][]; // in Lean: `Array (Name × Name)`
+  text: string
+  hidden: boolean
+  rawText: string
+  varNames?: string[][] // in Lean: `Array (Name × Name)`
 }
 
 export interface InteractiveGoalWithHints {
-  goal: InteractiveGoal;
-  hints: GameHint[];
+  goal: InteractiveGoal
+  hints: GameHint[]
 }
 
 export interface InteractiveGoalsWithHints {
-  goals: InteractiveGoalWithHints[];
-  command: string;
-  diags: any //InteractiveDiagnostic[];
+  goals: InteractiveGoalWithHints[]
+  command: string
+  diags: InteractiveDiagnostic[]
 }
 
 /**
@@ -74,11 +79,11 @@ export interface ProofState {
    *
    * In particular `step[i]` is the proof step at the beginning of line `i` in vscode.
    */
-  steps: InteractiveGoalsWithHints[];
+  steps: InteractiveGoalsWithHints[]
   /** The remaining diagnostics that are not in the steps. Usually this should only
    * be the "unsolved goals" message, I believe.
    */
-  diagnostics : any // InteractiveDiagnostic[];
-  completed : Boolean;
-  completedWithWarnings : Boolean;
+  diagnostics : InteractiveDiagnostic[]
+  completed : Boolean
+  completedWithWarnings : Boolean
 }

client/src/components/editor/Editor.tsx

@@ -2,7 +2,7 @@ import * as React from 'react';
 import Split from 'react-split'
 import { useContext, useEffect, useRef, useState } from 'react'
 import { useTranslation } from "react-i18next"
-import { GameIdContext } from '../../state/context';
+import { GameIdContext, MonacoEditorContext } from '../../state/context';
 import { useLoadLevelQuery } from '../../state/api';
 import { Markdown } from '../utils';
 import * as monaco from 'monaco-editor'
@@ -11,6 +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';
 
 export function Editor() {
   let { t } = useTranslation()
@@ -37,7 +38,12 @@ export function Editor() {
       window.location.host + `/websocket/${gameId}`
     console.log(`[LeanGame] socket url: ${socketUrl}`)
     var _options: LeanMonacoOptions = {
-      websocket: {url: socketUrl},
+      websocket: {
+        url: socketUrl,
+        // @ts-ignore
+        difficulty: 1,
+        inventory: []
+      },
       // Restrict monaco's extend (e.g. context menu) to the editor itself
       htmlElement: editorRef.current ?? undefined,
       vscode: {
@@ -69,7 +75,8 @@ export function Editor() {
     _leanMonaco.setInfoviewElement(infoviewRef.current!)
     ;(async () => {
         await _leanMonaco.start(options)
-        await leanMonacoEditor.start(editorRef.current!, `${gameId}/${worldId}/Level_${levelId}.lean`, code)
+        console.warn('gameId', gameId)
+        await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)
 
         setEditor(leanMonacoEditor.editor)
         setLeanMonaco(_leanMonaco)
@@ -85,9 +92,13 @@ export function Editor() {
     }
   }, [options, infoviewRef, editorRef, gameId, worldId, levelId])
 
-  return <Split direction='vertical' minSize={200} sizes={[50, 50]}
-        className={`editor-wrapper ${typewriterMode ? 'hidden' : ''}`} >
-      <div ref={editorRef} id="editor" />
-      <div ref={infoviewRef} id="infoview" />
-    </Split>
+  return <MonacoEditorContext.Provider value={editor}>
+    <div className="editor-wrapper"><Split direction='vertical' minSize={200} sizes={[50, 50]}
+          className={`editor-split ${typewriterMode ? 'hidden' : ''}`} >
+        <div ref={editorRef} id="editor" />
+        <div ref={infoviewRef} id="infoview" />
+      </Split>
+      {typewriterMode && <Typewriter />}
+    </div>
+  </MonacoEditorContext.Provider>
 }