Support multi-command snippets in MCP lean_run_at

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.

Start at the command-mode lean_run_at entry point and reproduce the failure with the minimal multi-command JSON request against Liris/BeamRunAtRepro.lean. Trace how command text and speculative state are handled, then verify that later commands see earlier ones, real document state remains unchanged, and plain requests discard derived state while handle variants retain only the final state.