refactor: Use consistent error handling

Pantograph/Goal.lean

@@ -6,7 +6,6 @@ All the functions starting with `try` resume their inner monadic state.
 import Pantograph.Tactic
 import Lean
 
-
 namespace Pantograph
 open Lean
 
@@ -141,8 +140,8 @@ protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n]
 
 private def restoreCoreMExtra (state : Core.SavedState) : CoreM Unit :=
   let { nextMacroScope, ngen, .. } := state
-  modifyGetThe Core.State (fun st => ((),
+  modifyGetThe Core.State fun st => ((),
-    { st with nextMacroScope, ngen }))
+    { st with nextMacroScope, ngen })
 -- Restore the name generator and macro scopes of the core state
 protected def GoalState.restoreCoreMExtra (state: GoalState): CoreM Unit :=
   restoreCoreMExtra state.coreState
@@ -469,7 +468,7 @@ protected def GoalState.step (state : GoalState) (site : Site) (tacticM : Elab.T
   : Elab.TermElabM GoalState :=
   Prod.snd <$> GoalState.step' state site tacticM guardMVarErrors
 
-/-- Response for executing a tactic -/
+/-- Result for executing a tactic, capturing errors in the process -/
 inductive TacticResult where
   -- Goes to next state
   | success (state : GoalState) (messages : Array Message)
@@ -480,40 +479,35 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message : String)
 
-private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (Bool × List Message) := do
+private def dumpMessageLog (prevMessageLength : Nat := 0) : CoreM (List Message) := do
   let newMessages := (← Core.getMessageLog).toList.drop prevMessageLength
-  let hasErrors := newMessages.any (·.severity == .error)
   Core.resetMessageLog
-  return (hasErrors, newMessages)
+  return newMessages
 
 /-- Execute a `TermElabM` producing a goal state, capturing the error and turn it into a `TacticResult` -/
 def withCapturingError (elabM : Elab.Term.TermElabM GoalState) : Elab.TermElabM TacticResult := do
   let messageLog ← Core.getMessageLog
   unless messageLog.toList.isEmpty do
     IO.eprintln s!"{← messageLog.toList.mapM (·.toString)}"
-    assert! messageLog.toList.isEmpty
+    throwError "Message log must be empty at the beginning."
   try
     let state ← elabM
 
     -- Check if error messages have been generated in the core.
-    let (hasError, newMessages) ← dumpMessageLog
+    let newMessages ← dumpMessageLog
-    if hasError then
+    let hasErrors := newMessages.any (·.severity == .error)
+    if hasErrors then
       return .failure newMessages.toArray
     else
       return .success state newMessages.toArray
   catch exception =>
-    match exception with
+    let messages ← dumpMessageLog
-    | .internal _ =>
+    let message := {
-      let (_, messages) ← dumpMessageLog
+      fileName := ← getFileName,
-      return .failure messages.toArray
+      pos := ← getRefPosition,
-    | _ =>
+      data := exception.toMessageData,
-      let (_, messages) ← dumpMessageLog
+    }
-      let message := {
+    return .failure (message :: messages).toArray
-        fileName := ← getFileName,
-        pos := ← getRefPosition,
-        data := exception.toMessageData,
-      }
-      return .failure (message :: messages).toArray
 
 /-- Executes a `TacticM` monad on this `GoalState`, collecting the errors as necessary -/
 protected def GoalState.tryTacticM

Test/Proofs.lean

@@ -352,8 +352,8 @@ def test_tactic_failure_synthesize_placeholder : TestM Unit := do
   --  buildGoal [("p", "Prop"), ("q", "Prop"), ("r", "Prop"), ("h", "p → q")] "p ∧ r"
   --]
 
-  let .failure #[message] ← state1.tacticOn 0 tactic
+  let .failure #[_head, message] ← state1.tacticOn 0 tactic
-    | addTest $ assertUnreachable s!"{tactic} should fail"
+    | addTest $ assertUnreachable s!"{tactic} should fail with 2 messages"
   checkEq s!"{tactic} fails" (← message.toString)
     s!"{← getFileName}:0:31: error: don't know how to synthesize placeholder\ncontext:\np q r : Prop\nh : p → q\n⊢ p ∧ r\n"