Rewrite eval-problem markers through Lean's parser rather than a lexical scan

stripProblemMarkers in EvalTools/Generate.lean walks Lean source with a hand-written lexer. #547 made that scan track comments, string, raw-string and character literals, French-quoted identifiers, syntax quotations and bracket depth, which is as far as lexing goes. Two ways of fooling it remain, and neither is reachable without the parser, because both turn on what the token table says rather than on what the characters are.

A token carrying a ) closes a syntax quotation early, so the text after it is read as code:

syntax "premature)" command : command

macro "mkHidden" : command =>
  `(premature)
    @[eval_problem] theorem hidden : True := trivial)

The marker belongs to the syntax the macro builds. The scan removes it.

A token carrying a " or a brace can likewise put the two readings of a string literal back into agreement on the wrong answer, defeating the Source.disputedStringEnd? test that otherwise stops the scan from reading a hole's contents as code.

Neither occurs in the catalog, and the failure needs a syntax declaration to reach. Both would go away if the pass located markers with Lean.Parser instead of by scanning, which is what sourceImports already does for imports. The obstacle is the signature: parsing wants an Environment, so stripProblemMarkers would become monadic, and a file declaring its own syntax would need that syntax available before it could be parsed. That is a design question rather than a patch, which is why it is filed separately from #544.

Found by OpenAI Codex reviewing #547.

🤖 Prepared with Claude Code

Start in EvalTools/Generate.lean with stripProblemMarkers, then compare its requirements with the sourceImports parser path. Investigate how parsing obtains an Environment and how file-local syntax declarations become available. Done means a documented design that handles syntax-defined files and both parser-dependent marker cases.