From 7cedfc5038cd5d030c9263f228b56b08407bf6d2 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sat, 6 Apr 2024 15:40:06 +0200
Subject: [PATCH] mark some server messages for translation

---
 server/GameServer/Commands.lean    |  1 +
 server/GameServer/RpcHandlers.lean | 11 ++++++++---
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 2b8faea1..648a253b 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -4,6 +4,7 @@ import GameServer.Options
 import GameServer.SaveData
 import GameServer.Hints
 import GameServer.Tactic.LetIntros
+import GameServer.RpcHandlers -- only needed to collect the translations of "level completed" msgs
 import I18n
 
 open Lean Meta Elab Command
diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean
index b4b75d7f..6ad15789 100644
--- a/server/GameServer/RpcHandlers.lean
+++ b/server/GameServer/RpcHandlers.lean
@@ -2,6 +2,7 @@ import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
 import Std.Data.Array.Init.Basic
 import GameServer.Hints
+import I18n
 
 open Lean
 open Server
@@ -171,7 +172,11 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
   if goalCount == 0 then
     if completed then
       out := out.push {
-        message := .text "level completed! 🎉"
+        -- TODO: marking these with `t!` has the implication that every game
+        -- needs to translate these messages again,
+        -- but cannot think of another option
+        -- that would not involve manually adding them somewhere in the translation files.
+        message := .text t!"level completed! 🎉"
         range := {
           start := pos
           «end» := pos
@@ -179,7 +184,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
         severity? := Lsp.DiagnosticSeverity.information }
     else if completedWithWarnings then
       out := out.push {
-        message := .text "level completed with warnings… 🎭"
+        message := .text t!"level completed with warnings… 🎭"
         range := {
           start := pos
           «end» := pos
@@ -192,7 +197,7 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
     -- so showing the message "intermediate goal solved" would be confusing.
     if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then
       out := out.push {
-        message := .text "intermediate goal solved! 🎉"
+        message := .text t!"intermediate goal solved! 🎉"
         range := {
           start := pos
           «end» := pos