[Merged by Bors] - feat: tweak calc widget

Mathlib/Tactic/Widget/Calc.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import Lean.Elab.Tactic.Calc
+import Lean.Meta.Tactic.TryThis
 
 import Mathlib.Data.String.Defs
 import Mathlib.Tactic.Widget.SelectPanelUtils
@@ -76,7 +77,8 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
   let mut goalType := goalType
   for pos in subexprPos do
     goalType ← insertMetaVar goalType pos
-  let some (_, newLhs, newRhs) ← Lean.Elab.Term.getCalcRelation? goalType | unreachable!
+  let some (_, newLhs, newRhs) ← Lean.Elab.Term.getCalcRelation? goalType |
+      throwError "invalid 'calc' step, relation expected{indentExpr goalType}"
 
   let lhsStr := (toString <| ← Meta.ppExpr lhs).renameMetaVar
   let newLhsStr := (toString <| ← Meta.ppExpr newLhs).renameMetaVar
@@ -115,7 +117,7 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
 /-- Rpc function for the calc widget. -/
 @[server_rpc_method]
 def CalcPanel.rpc := mkSelectionPanelRPC suggestSteps
-  "Please select subterms."
+  "Please select subterms using Shift-click."
   "Calc 🔍"
 
 /-- The calc widget. -/
@@ -124,19 +126,26 @@ def CalcPanel : Component CalcParams :=
   mk_rpc_widget% CalcPanel.rpc
 
 namespace Lean.Elab.Tactic
-open Meta
+
+open Lean Meta Tactic TryThis in
+/-- Create a `calc` proof. -/
+elab stx:"calc?" : tactic => withMainContext do
+  let goalType ← whnfR (← getMainTarget)
+  unless (← Lean.Elab.Term.getCalcRelation? goalType).isSome do
+    throwError "Cannot start a calculation here: the goal{indentExpr goalType}\nis not a relation."
+  let s ← `(tactic| calc $(← Lean.PrettyPrinter.delab (← getMainTarget)) := by sorry)
+  addSuggestions stx #[.suggestion s] (header := "Create calc tactic:")
+  evalTactic (← `(tactic|sorry))
 
 /-- Elaborator for the `calc` tactic mode variant with widgets. -/
 elab_rules : tactic
 | `(tactic|calc%$calcstx $steps) => do
-  let some calcRange := (← getFileMap).rangeOfStx? calcstx | unreachable!
-  let indent := calcRange.start.character
   let mut isFirst := true
   for step in ← Lean.Elab.Term.mkCalcStepViews steps do
-    let some replaceRange := (← getFileMap).rangeOfStx? step.ref | unreachable!
+    let some replaceRange := (← getFileMap).rangeOfStx? step.ref | continue
     let json := json% {"replaceRange": $(replaceRange),
                         "isFirst": $(isFirst),
-                        "indent": $(indent)}
+                        "indent": $(replaceRange.start.character)}
     Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) step.proof
     isFirst := false
   evalCalc (← `(tactic|calc%$calcstx $steps))

MathlibTest/CalcQuestionMark.lean

@@ -0,0 +1,67 @@
+import Mathlib.Tactic.Widget.Calc
+
+/-!
+Note that while the suggestions look incorrectly indented here,
+this is an artifact of the rendering to a string for `guard_msgs` (leanprover/lean4#7191).
+
+When used from the widget that appears in VSCode, they insert correctly-indented code.
+-/
+
+/--
+info: Create calc tactic:
+• calc
+  1 = 1 := by sorry
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example : 1 = 1 := by
+  have := 0
+  calc?
+
+
+/--
+info: Create calc tactic:
+• calc
+  a ≤ a := by sorry
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (a : Nat) : a ≤ a := by
+  calc?
+
+-- an indented `calc?`
+
+/--
+info: Create calc tactic:
+• calc
+  a ≤ a := by sorry
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (a : Nat) : a ≤ a := by
+  all_goals
+    calc?
+
+-- a deliberately long line
+/--
+info: Create calc tactic:
+• calc
+  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
+            1 +
+          1 +
+        1 =
+      8 + 8 + 8 + 8 :=
+    by sorry
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example :
+    1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
+    1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
+    1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 +
+    1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 = 8 + 8 + 8 + 8 := by
+  calc?