fix: make stripProblemMarkers lexer-aware rather than line-oriented

[kim-em]

This PR replaces the line-oriented marker stripper in EvalTools/Generate.lean with a scanner that walks the whole source, tracking line and block comments, string, raw-string and character literals, French-quoted identifiers, syntax quotations and bracket depth. The marker is now recognised in every position Lean accepts it: sharing a line with its declaration or with a prefix command such as include x in or set_option … in, spanning several lines, carrying trivia as in @[/- why -/ eval_problem], spelled «eval_problem», or carrying siblings whose arguments contain a ] or a ,. Surviving siblings are spliced out of the source rather than reprinted, so a comment among them keeps the line break that terminates it. Imports are parsed the same way, so one broken across lines or carrying a comment is recognised, while a doc comment trailing an import stays with the declaration it documents.

Lexing Lean without its parser cannot be exact: whether a { in a string opens an interpolation hole is settled by the grammar, and the grammar is extensible. Three things keep that inexactness from editing somebody's string. A marker is stripped only in command position and only in front of a declaration; and no span the two readings of a string literal disagree about is stripped from at all. The first two are tests on text, which a string can reproduce; the third is not a test on the marker but on how the scanner came to be looking at it, and reaching marker-shaped text inside a literal takes exactly the disagreement it declines to resolve. What is left over is a marker left in place, which the generated workspace reports as unknown attribute [eval_problem] when it is built.

Source.opaqueLexemeEnd? is the one place that knows how to step over a comment or a literal; Source.findTheoremBodyMarker now uses it in place of its own copy.

Nothing in the catalog exercises any of this today, so a differential check against the old implementation over every .lean file in LeanEval/, EvalTools/, tests/, generated/ and templates/ — in both shapes the generator passes in, with and without local-import stripping — reports no change in output.

Closes #544.

🤖 Prepared with Claude Code

[kim-em]

Reviewed by OpenAI Codex over six rounds; every reproducible finding is fixed and tested. The ones worth recording here, because they changed the design rather than the code:

• No lookback from a quote can decide whether a { opens an interpolation hole — Lean settles that in the parser, and the grammar is extensible. So the pass stopped depending on one being right: where the two readings of a literal disagree about where it ends, nothing in that span is stripped. That test is symmetric in the two readings, including when one of them never closes.
• No test on the text after a marker can be sound either, since a string can spell out @[eval_problem] theorem in full. Command position and the declaration that follows are still checked, but what makes marker-shaped text in a literal unreachable is the disputed-span test, which is about how the scan came to be looking at it.
• A doc comment after an import belongs to the declaration below it, not the import.

Measurements, since the corpus exercises none of this: a differential against the pre-#547 implementation over all 2015 .lean files in LeanEval/, EvalTools/, tests/, generated/ and templates/, in both shapes the generator passes in, reports no change in output; and appending a marker to each of Mathlib's 8312 files strips all 8312.

What is left needs a syntax declaration to reach and cannot be fixed by lexing, so it is #551 rather than a change here.