move Hint tactic back

server/GameServer/Commands.lean

@@ -464,6 +464,60 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 
 /-! # Hints -/
 
+open GameServer in
+
+/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
+see hints. The tactic does not affect the goal state.
+-/
+elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
+  let mut strict := false
+  let mut hidden := false
+
+  -- remove spaces at the beginning of new lines
+  let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
+    match m with
+    | Syntax.node info k args =>
+      if k == interpolatedStrLitKind && args.size == 1 then
+        match args.get! 0 with
+        | (Syntax.atom info' val) =>
+          let val := removeIndentation val
+          return Syntax.node info k #[Syntax.atom info' val]
+        | _ => return m
+      else
+        return m
+    | _ => return m
+
+  for arg in args do
+    match arg with
+    | `(hintArg| (strict := true)) => strict := true
+    | `(hintArg| (strict := false)) => strict := false
+    | `(hintArg| (hidden := true)) => hidden := true
+    | `(hintArg| (hidden := false)) => hidden := false
+    | _ => throwUnsupportedSyntax
+
+  let goal ← Tactic.getMainGoal
+  goal.withContext do
+    -- We construct an expression that can produce the hint text. The difficulty is that we
+    -- want the text to possibly contain quotation of the local variables which might have been
+    -- named differently by the player.
+    let varsName := `vars
+    let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
+      let mut text ← `(m! $msg)
+      let goalDecl ← goal.getDecl
+      let decls := goalDecl.lctx.decls.toArray.filterMap id
+      for i in [:decls.size] do
+        text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
+      return ← mkLambdaFVars #[vars] $ ← Term.elabTermAndSynthesize text none
+    let textmvar ← mkFreshExprMVar none
+    guard $ ← isDefEq textmvar text -- Store the text in a mvar.
+    -- The information about the hint is logged as a message using `logInfo` to transfer it to the
+    -- `Statement` command:
+    logInfo $
+      .tagged `Hint $
+      .nest (if strict then 1 else 0) $
+      .nest (if hidden then 1 else 0) $
+      .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
+
 /-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
 proof state. We use it to define Hints for alternative proof methods or dead ends. -/
 elab (name := GameServer.Tactic.Branch) "Branch" t:tacticSeq : tactic => do

server/GameServer/Hints.lean

@@ -52,55 +52,3 @@ partial def removeIndentation (s : String) : String :=
     else
       loop i (acc.push c)
   loop ⟨0⟩ ""
-
-/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
-see hints. The tactic does not affect the goal state.
--/
-elab (name := GameServer.Tactic.Hint) "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
-  let mut strict := false
-  let mut hidden := false
-
-  -- remove spaces at the beginning of new lines
-  let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
-    match m with
-    | Syntax.node info k args =>
-      if k == interpolatedStrLitKind && args.size == 1 then
-        match args.get! 0 with
-        | (Syntax.atom info' val) =>
-          let val := removeIndentation val
-          return Syntax.node info k #[Syntax.atom info' val]
-        | _ => return m
-      else
-        return m
-    | _ => return m
-
-  for arg in args do
-    match arg with
-    | `(hintArg| (strict := true)) => strict := true
-    | `(hintArg| (strict := false)) => strict := false
-    | `(hintArg| (hidden := true)) => hidden := true
-    | `(hintArg| (hidden := false)) => hidden := false
-    | _ => throwUnsupportedSyntax
-
-  let goal ← Tactic.getMainGoal
-  goal.withContext do
-    -- We construct an expression that can produce the hint text. The difficulty is that we
-    -- want the text to possibly contain quotation of the local variables which might have been
-    -- named differently by the player.
-    let varsName := `vars
-    let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
-      let mut text ← `(m! $msg)
-      let goalDecl ← goal.getDecl
-      let decls := goalDecl.lctx.decls.toArray.filterMap id
-      for i in [:decls.size] do
-        text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
-      return ← mkLambdaFVars #[vars] $ ← Term.elabTermAndSynthesize text none
-    let textmvar ← mkFreshExprMVar none
-    guard $ ← isDefEq textmvar text -- Store the text in a mvar.
-    -- The information about the hint is logged as a message using `logInfo` to transfer it to the
-    -- `Statement` command:
-    logInfo $
-      .tagged `Hint $
-      .nest (if strict then 1 else 0) $
-      .nest (if hidden then 1 else 0) $
-      .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)