fix: Rectify error format #31

Merged
aniva merged 1 commits from misc/error into dev 2023-11-25 14:26:48 -08:00
2 changed files with 5 additions and 6 deletions
Showing only changes of commit 2a9931c134 - Show all commits

View File

@ -193,7 +193,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
pure $ target.resume goals pure $ target.resume goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied" | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with match nextState? with
| .error error => return .ok { error? := .some error } | .error error => return .error <| errorI "structure" error
| .ok nextGoalState => | .ok nextGoalState =>
let nextStateId := state.nextId let nextStateId := state.nextId
set { state with 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) let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options)
return .ok { return .ok {
nextStateId? := .some nextStateId, nextStateId,
goals? := .some goals, goals,
} }
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get let state ← get

View File

@ -176,9 +176,8 @@ structure GoalContinue where
goals?: Option (List String) := .none goals?: Option (List String) := .none
deriving Lean.FromJson deriving Lean.FromJson
structure GoalContinueResult where structure GoalContinueResult where
error?: Option String := .none nextStateId: Nat
nextStateId?: Option Nat := .none goals: (Array Goal)
goals?: Option (Array Goal) := .none
deriving Lean.ToJson deriving Lean.ToJson
-- Remove goal states -- Remove goal states