fix: Rectify error format #31
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
Loading…
Reference in New Issue