Compare commits

..

No commits in common. "e4d53733d008bbda48c7d3513ac901fb4c3f3f12" and "9b3eef35ec40a09bba7140ecfc04dafddbd92c27" have entirely different histories.

2 changed files with 29 additions and 26 deletions

View File

@ -1,6 +1,6 @@
namespace Pantograph
@[export pantograph_version]
def version := "0.2.18"
def version := "0.2.17"
end Pantograph

View File

@ -169,7 +169,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}"
match state.goalStates.find? args.target with
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
| .some target => do
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates.find? branchId with
@ -198,9 +200,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}"
let result ← runMetaInMainM <| goalPrint goalState state.options
return .ok result
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => runMetaM <| do
return .ok (← goalPrint goalState state.options)
compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
let module := args.module.toName
try