Support multi-command snippets in MCP lean_run_at

[ejgallego]

Current status

lean_run_at now reports a clear semantic failure for top-level command sequences:

runAtSupportsOneCommandOnly: command-mode runAt accepts exactly one Lean command...

That fixed the confusing raw expected end of input symptom and documents the current one-command contract. It is not the desired final behavior for this issue.

Requested behavior

Support complete Lean command sequences in command-mode lean_run_at at a source position. For example, this should execute as one speculative request:

def beamRunAtA : Nat := 1

def beamRunAtB : Nat := beamRunAtA

#check beamRunAtB

Later commands in the snippet should see earlier commands from the same snippet, while the request still behaves like an isolated runAt sandbox:

• do not mutate the real document elaboration state
• do not depend on side effects from previous requests
• discard derived execution state after plain lean_run_at
• for handle-storing variants, store the final command state after the sequence only when the API explicitly asks for a handle

Minimal reproduction

Create a clean module:

def beamRunAtBase : Nat := 0

A single command works:

{
  "tool": "lean_run_at",
  "arguments": {
    "path": "Liris/BeamRunAtRepro.lean",
    "line": 1,
    "character": 0,
    "text": "#check beamRunAtBase"
  }
}

A complete multi-command snippet currently fails with runAtSupportsOneCommandOnly:

{
  "tool": "lean_run_at",
  "arguments": {
    "path": "Liris/BeamRunAtRepro.lean",
    "line": 1,
    "character": 0,
    "text": "def beamRunAtA : Nat := 1\n\ndef beamRunAtB : Nat := beamRunAtA\n\n#check beamRunAtB"
  }
}

Relationship to batch runAt

This is separate from #101. Multi-command support lets one snippet elaborate as ordinary Lean command text. Batch runAt is still useful for several independent probes with per-item results.

Agent impact

This would reduce friction for common source-position probes such as declaring a helper and immediately checking a consumer, without writing scratch files or reconstructing context outside the real module.