diff --git a/Pantograph.lean b/Pantograph.lean index 6ec4ac1..a1f2602 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -29,17 +29,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do | .error ierror => return Lean.toJson ierror | .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}" match command.cmd with - | "reset" => run reset - | "stat" => run stat - | "expr.echo" => run expr_echo - | "lib.catalog" => run lib_catalog - | "lib.inspect" => run lib_inspect - | "options.set" => run options_set - | "options.print" => run options_print - | "goal.start" => run goal_start - | "goal.tactic" => run goal_tactic - | "goal.continue" => run goal_continue - | "goal.delete" => run goal_delete + | "reset" => run reset + | "stat" => run stat + | "expr.echo" => run expr_echo + | "lib.catalog" => run lib_catalog + | "lib.inspect" => run lib_inspect + | "options.set" => run options_set + | "options.print" => run options_print + | "goal.start" => run goal_start + | "goal.tactic" => run goal_tactic + | "goal.continue" => run goal_continue + | "goal.delete" => run goal_delete | "goal.print" => run goal_print | cmd => let error: Protocol.InteractionError :=