check when level is completed

fixes #27

client/src/components/Level.tsx

@@ -194,7 +194,7 @@ function Level() {
 
 
           <EditorContext.Provider value={editorConnection}>
-            {editorConnection && <Main key={`${worldId}/${levelId}`}/>}
+            {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
           </EditorContext.Provider>
         </Grid>
       </Grid>

client/src/components/infoview/infoview.css

@@ -30,3 +30,8 @@
   font-size: 1.5rem;
   font-weight: 500;
 }
+
+.level-completed {
+  font-size: 1.8rem;
+  font-weight: 500;
+}

client/src/components/infoview/main.tsx

@@ -1,7 +1,7 @@
 /* Partly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/main.tsx */
 
 import * as React from 'react';
-import type { DidCloseTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
+import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, DocumentUri } from 'vscode-languageserver-protocol';
 
 import 'tachyons/css/tachyons.css';
 // import '@vscode/codicons/dist/codicon.ttf';
@@ -13,15 +13,35 @@ import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoview
 
 import { Infos } from './infos';
 import { AllMessages, WithLspDiagnosticsContext } from './messages';
-import { useClientNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion';
+import { useAppDispatch, useAppSelector } from '../../hooks';
+import { codeEdited, levelCompleted, selectCompleted } from '../../state/progress';
 
 
-export function Main(props: {}) {
+export function Main(props: {world: string, level: number}) {
     const ec = React.useContext(EditorContext);
 
+    const dispatch = useAppDispatch()
+
+    // Mark level as completed when server gives notification
+    useServerNotificationEffect(
+        '$/game/completed',
+        (params: any) => {
+
+            if (ec.events.changedCursorLocation.current &&
+                ec.events.changedCursorLocation.current.uri === params.uri) {
+                dispatch(codeEdited)
+            }
+            dispatch(levelCompleted({world: props.world, level: props.level}))
+        },
+        []
+    );
+
+    const completed = useAppSelector(selectCompleted(props.world, props.level))
+
     /* Set up updates to the global infoview state on editor events. */
     const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
 
@@ -61,6 +81,7 @@ export function Main(props: {}) {
         ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
     } else {
         ret = <div className="ma1 infoview vscode-light">
+            {completed && <div className="level-completed">Level completed! 🎉</div>}
             <Infos />
         </div>
     }

server/leanserver/GameServer/FileWorker.lean

@@ -155,6 +155,19 @@ where
   private def publishIleanInfoFinal : DocumentMeta → FS.Stream → Array Snapshot → IO Unit :=
     publishIleanInfo "$/lean/ileanInfoFinal"
 
+  structure GameCompletedParams where
+    uri : String
+  deriving ToJson, FromJson
+
+  /-- Checks whether game level has been completed and sends a notification to the client -/
+  def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
+    -- check if there is any error or warning
+    for snap in snaps do
+      if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
+      then return
+    let param := { uri := m.uri : GameCompletedParams}
+    hOut.writeLspNotification { method := "$/game/completed", param }
+
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
       : AsyncElabM (Option Snapshot) := do
@@ -162,6 +175,7 @@ where
     let s ← get
     let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
     if lastSnap.isAtEnd then
+      publishGameCompleted m ctx.hOut s.snaps
       publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
       publishProgressDone m ctx.hOut
       -- This will overwrite existing ilean info for the file, in case something