work on proxy: wrap sample code around editor

client/src/components/editor/Editor.tsx

@@ -84,7 +84,7 @@ export function Editor() {
         // let infoProvider = _leanMonaco.infoProvider.editorApi
 
         console.warn('gameId', gameId)
-        await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)
+        await leanMonacoEditor.start(editorRef.current!, `/${gameId}/${worldId}/L_${levelId}.lean`, code)
 
         setEditor(leanMonacoEditor.editor)
         setLeanMonaco(_leanMonaco)

server/GameServerExe.lean

@@ -1,4 +1,5 @@
 import GameServerExe.Rpc
+import GameServer
 import GameServerExe.Message
 import Lake.CLI.Main
 
@@ -56,17 +57,27 @@ unsafe def main : List String → IO UInt32 := fun args => do
     let o_lean : IO.FS.Stream := .ofHandle leanProcess.stdout
     -- let e_lean : IO.FS.Stream := .ofHandle leanProcess.stderr
 
-    while true do
-      /- redirect message from the client to the server -/
+    -- Test: import game info from `Game`'s env
+    initSearchPath (← findSysroot)
+    unsafe Lean.withImportModules #[`TestGame] {} (trustLevel := 1024)
+      fun env => Prod.fst <$> Core.CoreM.toIO
+          ( ctx := { fileName := "<CoreM>", fileMap := default })
+          (s := { env := env }) do
 
-      let msgI : JsonRpc.Message := GameServer.forwardMessage (← i.readLspMessage)
-      i_lean.writeLspMessage msgI
+        -- get the game from the Env
+        let game ← GameServer.getCurGame
+        debug_msg s!"cwd: {(← IO.currentDir)}"
 
-      let msgO : JsonRpc.Message := GameServer.returnMessage (← o_lean.readLspMessage)
-      o.writeLspMessage msgO
+        while true do
+          /- redirect message from the client to the server -/
+          let msgI : JsonRpc.Message ← GameServer.forwardMessage (← i.readLspMessage)
+          i_lean.writeLspMessage msgI
 
-      -- let msgE : JsonRpc.Message ← e_lean.readLspMessage
-      -- e.writeLspMessage msgE
+          let msgO : JsonRpc.Message ← GameServer.returnMessage (← o_lean.readLspMessage)
+          o.writeLspMessage msgO
+
+          -- let msgE : JsonRpc.Message ← e_lean.readLspMessage
+          -- e.writeLspMessage msgE
 
     IO.Process.exit 0
   catch err =>

server/GameServerExe/Message.lean

@@ -1,18 +1,107 @@
 import Lean
-
--- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
--- should we have a different solution?
+import GameServer.Layer.Extension
 
 set_option linter.unusedVariables false
 
 namespace GameServer
 
 open Lean
 
+def createDebugNotification (msg : String) : JsonRpc.Message :=
+  let params : Json.Structured := .arr #[msg] -- TODO: didn't know how to create a `.obj`
+  .notification "lean4game/debug" params
+
+/--
+Send debug messages as `lean4game/debug` RPC notification.
+
+Can be used to print debug messages from within `GameServerExe` to the server console.
+
+Currently they are ignored by the frontend, but in dev mode they
+appear as `DEBUG:` message in the server's shell (see `relay/index.mjs`)
+-/
+def _root_.debug_msg (msg : String) : IO Unit := do
+  let o ← IO.getStdout
+  o.writeLspMessage (createDebugNotification msg)
+
+def getLevelIdFromUri (game : Game) (uri : String) : LevelId :=
+  let components := uri.split ("\\/_.".contains ·)
+  match components.reverse with
+    | "lean" :: lvl :: "L" :: worldId :: gameId ::_ =>
+      { game := game.name,
+        world := .mkSimple worldId,
+        level := lvl.toNat! }
+    | _ => panic! s!"[GameServer] ERROR: bad URI '{uri}'"
+
+/--
+Takes the JSON of an element of `contentChanges` in the rpc notif. `textDocument/didChange`
+and applies the `shift` to all ranges.
+-/
+def shiftRange (shift : Nat → Nat) (change : Json) : Json := Id.run do
+  let mut range := change.getObjValD "range"
+  let mut start := range.getObjValD "start"
+  let mut «end» := range.getObjValD "end"
+  let .ok startLine := start.getObjValAs? Nat "line"
+    | panic! "[GameServer] unhandled"
+  let .ok endLine := end.getObjValAs? Nat "line"
+    | panic! "[GameServer] unhandled"
+  start := start.setObjValAs! "line" (shift startLine)
+  «end» := «end».setObjValAs! "line" (shift endLine)
+  range := range.setObjVal! "start" start
+  range := range.setObjVal! "end" «end»
+  change.setObjVal! "range" range
+
 /-- Redirect message from the client to the Lean server. -/
-def forwardMessage (msg : JsonRpc.Message) : JsonRpc.Message := Id.run do
+def forwardMessage (msg : JsonRpc.Message) : CoreM JsonRpc.Message := do
+  let game ← GameServer.getCurGame
   match msg with
+    | .notification "initialized" params? =>
+      return msg
+    | .notification method@("textDocument/didOpen") none =>
+      debug_msg s!"BUG: I thought receiving 'textDocument/didOpen' without params was impossible"
+      IO.Process.exit 2
+    | .notification method@("textDocument/didOpen") (some params') =>
+      let mut params : Json := ToJson.toJson params'
+      let textDocument := params.getObjValD "textDocument"
+      let .ok content := textDocument.getObjValAs? String "text"
+        | panic! s!"[GameServer]: ERROR: received didOpen notification with invalid parameters!"
+      let .ok uri := textDocument.getObjValAs? String "uri"
+        | panic! s!"[GameServer]: ERROR: received didOpen notification with invalid parameters!"
+
+      -- URI example: `file:///mygame/DemoWorld1/L_1.lean`
+      -- TODO: is this also true on Windows?
+
+      let levelId := getLevelIdFromUri game uri
+      debug_msg s!"[GameServer] `didOpen` {levelId}"
+      let some level ← getLevel? levelId
+        | panic! "[GameServer] Level not found"
+
+      let template := s!"example : True := by\n{content}\ndone"
+
+      params := params.setObjVal! "textDocument" (textDocument.setObjVal! "text" template)
+      let .ok paramsStructured := Json.toStructured? params
+        | panic! "[GameServer] unhandled"
+
+      return .notification method paramsStructured
+    -- textDocument/didChange
+
+    | .notification method@("textDocument/didChange") (some params') =>
+      let mut params : Json := ToJson.toJson params'
+      let textDocument := params.getObjValD "textDocument"
+      let .ok contentChanges := (params.getObjValD "contentChanges").getArr?
+        | panic! "[GameServer] unhandled"
+
+      let contentChangeNew : Json := .arr <| contentChanges.map (shiftRange (·+1))
+
+      params := params.setObjVal! "contentChanges" contentChangeNew
+      let .ok paramsStructured := Json.toStructured? params
+        | panic! "[GameServer] unhandled"
+      debug_msg s!"{params}"
+      return .notification method paramsStructured
+
+
     | .request id method params? =>
+      debug_msg s!"TODO client request {method} not implemented!"
+
       /-
       monaco requests to modify:
 
@@ -33,36 +122,24 @@ def forwardMessage (msg : JsonRpc.Message) : JsonRpc.Message := Id.run do
       -/
       return msg
     | .notification method params? =>
+      debug_msg s!"TODO client notification {method} not implemented!"
       return msg
     | .response id result =>
       return msg
     | .responseError id code message data? =>
       return msg
 
 /-- Redirect message from the Lean server back to the client. -/
-def returnMessage (msg : JsonRpc.Message) : JsonRpc.Message := Id.run do
+def returnMessage (msg : JsonRpc.Message) : CoreM JsonRpc.Message := do
+  let game ← GameServer.getCurGame
   match msg with
     | .request id method params? =>
+      debug_msg s!"TODO server request {method} not implemented!"
       return msg
     | .notification method params? =>
+      debug_msg s!"TODO server notification {method} not implemented!"
       return msg
     | .response id result =>
       return msg
     | .responseError id code message data? =>
       return msg
-
-def createDebugNotification (msg : String) : JsonRpc.Message :=
-  let params : Json.Structured := .arr #[msg] -- TODO: didn't know how to create a `.obj`
-  .notification "lean4game/debug" params
-
-/--
-Send debug messages as `lean4game/debug` RPC notification.
-
-Can be used to print debug messages from within `GameServerExe` to the server console.
-
-Currently they are ignored by the frontend, but in dev mode they
-appear as `DEBUG:` message in the server's shell (see `relay/index.mjs`)
--/
-def _root_.debug_msg (msg : String) : IO Unit := do
-  let o ← IO.getStdout
-  o.writeLspMessage (createDebugNotification msg)