feat: unify goal handlers

src/Lean/Server/FileWorker/RequestHandling.lean

@@ -13,6 +13,8 @@ import Lean.Server.FileWorker.Utils
 import Lean.Server.Requests
 import Lean.Server.Completion
 
+import Lean.Widget.InteractiveGoal
+
 namespace Lean.Server.FileWorker
 open Lsp
 open RequestM
@@ -133,54 +135,66 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
               return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
       return #[]
 
-open Elab in
-partial def handlePlainGoal (p : PlainGoalParams)
-    : RequestM (RequestTask (Option PlainGoal)) := do
+open RequestM in
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask Widget.InteractiveGoals) := do
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
   -- NOTE: use `>=` since the cursor can be *after* the input
   withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
-    (notFoundX := return none) fun snap => do
+    (notFoundX := return { goals := #[] }) fun snap => do
       for t in snap.cmdState.infoState.trees do
         if let rs@(_ :: _) := t.goalsAt? doc.meta.text hoverPos then
           let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
             let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
             let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
-            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Meta.ppGoal g))
-          let md :=
-            if goals.isEmpty then
-              "no goals"
-            else
-              let goals := goals.map fun goal => s!"```lean
-{goal}
-```"
-              String.intercalate "\n---\n" goals
-          return some { goals := goals.map toString |>.toArray, rendered := md }
+            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (Widget.goalToInteractive g))
+          return { goals := goals.toArray }
 
-      return none
+      return { goals := #[] }
 
 open Elab in
-open Meta in
-partial def handlePlainTermGoal (p : PlainTermGoalParams)
-    : RequestM (RequestTask (Option PlainTermGoal)) := do
+partial def handlePlainGoal (p : PlainGoalParams)
+    : RequestM (RequestTask (Option PlainGoal)) := do
+  let t ← getInteractiveGoals p
+  t.map <| Except.map fun ⟨goals⟩ =>
+    if goals.isEmpty then
+      some { goals := #[], rendered := "no goals" }
+    else
+      let goalStrs := goals.map (toString ·.pretty)
+      let goalBlocks := goalStrs.map fun goal => s!"```lean
+{goal}
+```"
+      let md := String.intercalate "\n---\n" goalBlocks.toList
+      some { goals := goalStrs, rendered := md }
+
+partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
+    : RequestM (RequestTask (Option (Widget.InteractiveGoal × Range))) := do
   let doc ← readDoc
   let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
   withWaitFindSnap doc (fun s => s.endPos > hoverPos)
     (notFoundX := pure none) fun snap => do
       for t in snap.cmdState.infoState.trees do
-        if let some (ci, i@(Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
-          let ty ← ci.runMetaM i.lctx do
-            instantiateMVars <| ti.expectedType?.getD (← inferType ti.expr)
-          -- for binders, hide the last hypothesis (the binder itself)
-          let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
-          let goal ← ci.runMetaM lctx' do
-            withPPInaccessibleNames <| Meta.ppGoal (← mkFreshExprMVar ty).mvarId!
-          let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
-          return some { goal := toString goal, range }
+        if let some (ci, i@(Elab.Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
+         let ty ← ci.runMetaM i.lctx do
+           Meta.instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
+         -- for binders, hide the last hypothesis (the binder itself)
+         let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
+         let goal ← ci.runMetaM lctx' do
+           Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
+         let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
+         return some (goal, range)
       return none
 
+def handlePlainTermGoal (p : PlainTermGoalParams)
+    : RequestM (RequestTask (Option PlainTermGoal)) := do
+  let t ← getInteractiveTermGoal p
+  t.map <| Except.map <| Option.map fun (goal, range) =>
+    { goal := toString goal.pretty
+      range := range
+    }
+
 partial def handleDocumentHighlight (p : DocumentHighlightParams)
     : RequestM (RequestTask (Array DocumentHighlight)) := do
   let doc ← readDoc

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -9,6 +9,7 @@ import Lean.Widget.InteractiveGoal
 import Lean.Widget.InteractiveDiagnostic
 
 import Lean.Server.Rpc.RequestHandling
+import Lean.Server.FileWorker.RequestHandling
 
 /-! Registers all widget-related RPC procedures. -/
 
@@ -72,56 +73,20 @@ builtin_initialize
           doc := ← i.info.docString? : InfoPopup
         }
 
-open RequestM in
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask InteractiveGoals) := do
-  let doc ← readDoc
-  let text := doc.meta.text
-  let hoverPos := text.lspPosToUtf8Pos p.position
-  -- NOTE: use `>=` since the cursor can be *after* the input
-  withWaitFindSnap doc (fun s => s.endPos >= hoverPos)
-    (notFoundX := return { goals := #[] }) fun snap => do
-      for t in snap.cmdState.infoState.trees do
-        if let rs@(_ :: _) := t.goalsAt? doc.meta.text hoverPos then
-          let goals ← List.join <$> rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter } =>
-            let ci := if useAfter then { ci with mctx := ti.mctxAfter } else { ci with mctx := ti.mctxBefore }
-            let goals := if useAfter then ti.goalsAfter else ti.goalsBefore
-            ci.runMetaM {} <| goals.mapM (fun g => Meta.withPPInaccessibleNames (goalToInteractive g))
-          return { goals := goals.toArray }
-
-      return { goals := #[] }
-
-open RequestM in
-partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
-    : RequestM (RequestTask (Option InteractiveGoal)) := do
-  let doc ← readDoc
-  let text := doc.meta.text
-  let hoverPos := text.lspPosToUtf8Pos p.position
-  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
-    (notFoundX := pure none) fun snap => do
-      for t in snap.cmdState.infoState.trees do
-        if let some (ci, i@(Elab.Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
-         let ty ← ci.runMetaM i.lctx do
-           Meta.instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
-         -- for binders, hide the last hypothesis (the binder itself)
-         let lctx' := if ti.isBinder then i.lctx.pop else i.lctx
-         let goal ← ci.runMetaM lctx' do
-           Meta.withPPInaccessibleNames <| goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId!
-         --let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
-         return some goal
-      return none
-
 builtin_initialize
   registerRpcCallHandler
     `Lean.Widget.getInteractiveGoals
     Lsp.PlainGoalParams
     InteractiveGoals
-    getInteractiveGoals
+    FileWorker.getInteractiveGoals
 
   registerRpcCallHandler
     `Lean.Widget.getInteractiveTermGoal
     Lsp.PlainTermGoalParams
     (Option InteractiveGoal)
-    getInteractiveTermGoal
+    fun p => do
+      let t ← FileWorker.getInteractiveTermGoal p
+      t.map <| Except.map <| Option.map Prod.fst
 
 open RequestM in
 def getInteractiveDiagnostics (_ : Json) : RequestM (RequestTask (Array InteractiveDiagnostic)) := do

src/Lean/Widget/InteractiveGoal.lean

@@ -7,8 +7,6 @@ Authors: Wojciech Nawrocki
 import Lean.Widget.InteractiveCode
 
 /-! RPC procedures for retrieving tactic and term goals with embedded `CodeWithInfos`. -/
--- TODO(WN): this module is mostly a slightly adapted copy of the corresponding `plainGoal/plainTemGoal` handlers
--- unify them
 
 namespace Lean.Widget
 open Server
@@ -33,7 +31,7 @@ private def addLine (fmt : Format) : Format :=
 def pretty (g : InteractiveGoal) : Format := do
   let indent := 2 -- Use option
   let mut ret := match g.userName? with
-    | some userName => f!"case {userName}{Format.line}"
+    | some userName => f!"case {userName}"
     | none          => Format.nil
   for hyp in g.hyps do
     ret := addLine ret
@@ -105,7 +103,8 @@ def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
         else
           ppVars varNames prevType? hyps localDecl
     let hyps ← pushPending varNames type? hyps
-    let goalFmt ← exprToInteractive mvarDecl.type
+    let goalTp ← instantiateMVars mvarDecl.type
+    let goalFmt ← exprToInteractive goalTp
     let userName? := match mvarDecl.userName with
       | Name.anonymous => none
       | name           => some <| toString name.eraseMacroScopes

tests/lean/interactive/editAfterError.lean.expected.out

@@ -40,3 +40,21 @@
    "fullRange":
    {"start": {"line": 1, "character": 7},
     "end": {"line": 1, "character": 11}}}]}
+{"version": 2,
+ "uri": "file://editAfterError.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}},
+   "message": "unknown identifier 'tru'",
+   "fullRange":
+   {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}},
+  {"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}},
+   "message": "unknown identifier 'fals'",
+   "fullRange":
+   {"start": {"line": 1, "character": 7},
+    "end": {"line": 1, "character": 11}}}]}

tests/lean/interactive/unterminatedDocComment.lean.expected.out

@@ -4,3 +4,5 @@
    "range":
    {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 3}}}]}
 {"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []}
+{"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []}
+{"version": 2, "uri": "file://unterminatedDocComment.lean", "diagnostics": []}