refactor: make throwTacticEx parameter msg optional (#3951)

previously, the empty `MessageData` (`m!""`) was used to indicate “no
message”, and `throwTacticEx` would format the message differently then.
But the semantics of `MessageData.isEmpty` isn't entirely clear in the
presence of lazy message data (e.g. `.ofPPFormat`).

So to avoid wondering what `isEmpty` should do there, let's simply use
an optional argument to `throwTacticEx` and get rid of
`MessageData.isEmpty`.

src/Lean/Elab/Tactic/Split.lean

@@ -21,12 +21,12 @@ open Meta
       throwErrorAt stx[2] "'split' tactic failed, select a single target to split"
     if simplifyTarget then
       liftMetaTactic fun mvarId => do
-       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
+       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId
         return mvarIds
     else
       let fvarId ← getFVarId hyps[0]!
       liftMetaTactic fun mvarId => do
-        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId ""
+        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId
         return mvarIds
   | Location.wildcard =>
     liftMetaTactic fun mvarId => do
@@ -34,7 +34,7 @@ open Meta
       for fvarId in fvarIds do
         if let some mvarIds ← splitLocalDecl? mvarId fvarId then
           return mvarIds
-      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
+      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId
       return mvarIds
 
 end Lean.Elab.Tactic

src/Lean/Message.lean

@@ -82,17 +82,6 @@ inductive MessageData where
 
 namespace MessageData
 
-/-- Determines whether the message contains any content. -/
-def isEmpty : MessageData → Bool
-  | ofFormat f => f.isEmpty
-  | withContext _ m => m.isEmpty
-  | withNamingContext _ m => m.isEmpty
-  | nest _ m => m.isEmpty
-  | group m => m.isEmpty
-  | compose m₁ m₂ => m₁.isEmpty && m₂.isEmpty
-  | tagged _ m => m.isEmpty
-  | _ => false
-
 variable (p : Name → Bool) in
 /-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. -/
 partial def hasTag : MessageData → Bool

src/Lean/Meta/Tactic/Assumption.lean

@@ -33,7 +33,7 @@ def assumptionCore (mvarId : MVarId) : MetaM Bool :=
 /-- Close goal `mvarId` using an assumption. Throw error message if failed. -/
 def _root_.Lean.MVarId.assumption (mvarId : MVarId) : MetaM Unit :=
   unless (← mvarId.assumptionCore) do
-    throwTacticEx `assumption mvarId ""
+    throwTacticEx `assumption mvarId
 
 @[deprecated MVarId.assumption]
 def assumption (mvarId : MVarId) : MetaM Unit :=

src/Lean/Meta/Tactic/Contradiction.lean

@@ -224,7 +224,7 @@ Throw exception if goal failed to be closed.
 -/
 def _root_.Lean.MVarId.contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=
   unless (← mvarId.contradictionCore config) do
-    throwTacticEx `contradiction mvarId ""
+    throwTacticEx `contradiction mvarId
 
 @[deprecated MVarId.contradiction]
 def contradiction (mvarId : MVarId) (config : Contradiction.Config := {}) : MetaM Unit :=

src/Lean/Meta/Tactic/Refl.lean

@@ -67,6 +67,6 @@ Close given goal using `HEq.refl`.
 def _root_.Lean.MVarId.hrefl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do
     let some [] ← observing? do mvarId.apply (mkConst ``HEq.refl [← mkFreshLevelMVar])
-      | throwTacticEx `hrefl mvarId ""
+      | throwTacticEx `hrefl mvarId
 
 end Lean.Meta

src/Lean/Meta/Tactic/Util.lean

@@ -36,11 +36,10 @@ def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do
 def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous) : MetaM Expr :=
   mkFreshExprMVar type MetavarKind.syntheticOpaque tag
 
-def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg : MessageData) : MetaM α :=
-  if msg.isEmpty then
-    throwError "tactic '{tacticName}' failed\n{mvarId}"
-  else
-    throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}"
+def throwTacticEx (tacticName : Name) (mvarId : MVarId) (msg? : Option MessageData := none) : MetaM α :=
+  match msg? with
+  | none => throwError "tactic '{tacticName}' failed\n{mvarId}"
+  | some msg => throwError "tactic '{tacticName}' failed, {msg}\n{mvarId}"
 
 def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do
   throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"