Pantograph/Version.lean

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

Repl.lean

@@ -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}"
+    match state.goalStates.find? args.stateId with
-    let result ← runMetaInMainM <| goalPrint goalState state.options
+    | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    return .ok result
+    | .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