chore: Version 0.3 #136
|
@ -79,6 +79,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
||||||
let state ← get
|
let state ← get
|
||||||
let nGoals := state.goalStates.size
|
let nGoals := state.goalStates.size
|
||||||
set { state with nextId := 0, goalStates := .empty }
|
set { state with nextId := 0, goalStates := .empty }
|
||||||
|
Lean.Core.resetMessageLog
|
||||||
return .ok { nGoals }
|
return .ok { nGoals }
|
||||||
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
|
||||||
let state ← get
|
let state ← get
|
||||||
|
|
Loading…
Reference in New Issue