From 2a9931c134f2bfd55f09bea853b53b512eede06a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 9 Nov 2023 22:24:17 -0800
Subject: [PATCH] fix: Rectify error format

---
 Pantograph.lean          | 6 +++---
 Pantograph/Protocol.lean | 5 ++---
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index f9f8cc6..f456e81 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -193,7 +193,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           pure $ target.resume goals
         | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
       match nextState? with
-      | .error error => return .ok { error? := .some error }
+      | .error error => return .error <| errorI "structure" error
       | .ok nextGoalState =>
         let nextStateId := state.nextId
         set { state with
@@ -202,8 +202,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         }
         let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options)
         return .ok {
-          nextStateId? := .some nextStateId,
-          goals? := .some goals,
+          nextStateId,
+          goals,
         }
   goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
     let state ← get
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index ce42d9d..c01228d 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -176,9 +176,8 @@ structure GoalContinue where
   goals?: Option (List String) := .none
   deriving Lean.FromJson
 structure GoalContinueResult where
-  error?: Option String := .none
-  nextStateId?: Option Nat := .none
-  goals?: Option (Array Goal) := .none
+  nextStateId: Nat
+  goals: (Array Goal)
   deriving Lean.ToJson
 
 -- Remove goal states