Iterative execution of proofs

A common use case for the repl is writing proofs tactic by tactic. Currently, this requires re-executing the entire head of the source file. It would be great if we could iteratively execute tactic proofs. For example, I would want to be able to input

{ "cmd" : "import Mathlib.Algebra.Order.Ring.Abs\nimport Mathlib.Data.Nat.Order.Basic\nimport Mathlib.Tactic.Ring\n\nopen List\n\nexample (α : Type) (L M : List α) : (L ++ M ++ L).length = (M ++ L ++ L).length := by\n  simp\n" }

followed by

{ "cmd" : "  ring" , "env" : 0 }

Currently, the latter returns

{"sorries": [],
 "messages":
 [{"severity": "error",
   "pos": {"line": 2, "column": 2},
   "endPos": null,
   "data": "expected command"}],
 "env": 1}

Start with the REPL handling of the JSON cmd and env fields and trace how the first proof input establishes environment 0. Reproduce the second input containing ring; done means tactic text can be executed incrementally against that environment without the current “expected command” error.