feat(semantic): scope document-text cartouche bodies as documentation

[Arthur742Ramos]

What

Scopes the body of document-markup commands (chapter / section /
subsection / subsubsection / paragraph / subparagraph / text /
txt / text_raw) as documentation (comment-like) instead of a generic
cartouche string.

Why

text ‹…› and section headings are formal document prose; Isabelle/jEdit
renders them distinctly from inner-syntax cartouches. Colouring them as a plain
quoted string under-sells that distinction. This makes the editor read the way
the document model intends.

Behaviour

• @{…} antiquotations, \<…> symbols, and nested cartouches inside the
  prose stay highlighted.
• Plain cartouches elsewhere (definition … where ‹…›, inner-syntax terms)
  are unaffected — only doc-command bodies change.
• Both Unicode ‹…› and ASCII \<open>…\<close> openers are handled.

How tested

• Real vscode-textmate + vscode-oniguruma tokenization of
  section ‹Intro @{term x}›, text ‹… \<lambda> … ‹nested› …›,
  lemma foo: "…", and definition … where \<open>not doc\<close> —
  doc bodies scope as comment.block.documentation, antiquotations/symbols
  remain highlighted, nesting is correct, and non-doc cartouches/strings are
  unchanged.
• npm run check — 1226 tests pass (new structural assertion pins the patterns).
• npm run bundle — clean.

[Copilot]

Pull request overview

This PR updates the Isabelle TextMate grammar so that cartouche bodies of document-markup commands (e.g. section ‹…›, text \<open>…\<close>) are scoped as documentation (comment.block.documentation.isabelle) rather than as a generic cartouche string, making prose render more like Isabelle/jEdit while preserving nested highlighting (antiquotations, symbols, nested cartouches).

Changes:

• Add dedicated documentation-unicode / documentation-ascii grammar rules and place them before the generic cartouche patterns.
• Add/extend a drift-style grammar manifest test to assert repository entries exist, have the right scopes, and are ordered correctly.
• Document the new highlighting behavior in CHANGELOG.md (currently needs a small fix—see comment).

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
syntaxes/isabelle.tmLanguage.json	Adds documentation cartouche patterns and ensures they take precedence over generic cartouches.
test/syntaxes/isabelleGrammar.test.ts	Extends grammar-manifest assertions to pin documentation scoping and pattern ordering.
CHANGELOG.md	Notes the new document-text scoping behavior (but currently merges two bullets unintentionally).

Comments suppressed due to low confidence (1)

CHANGELOG.md:22

• This changelog entry accidentally absorbs the next bullet’s content (the find_unused_assms/nunchaku/… list) into the new “Document-text reads as prose” item, because the diagnostic-commands bullet heading was removed but its continuation lines remain. This makes the “Added” section misleading and hard to read.

  cartouches elsewhere (e.g. `definition … where ‹…›`) are unaffected. Offline.
  `find_unused_assms`, `nunchaku`, `test_code`, the `print_bnfs` /
  `print_claset` / `print_induct_rules` / `print_coercions` / `print_record` /
  `print_case_translations` / `print_quotients` / `print_quotconsts` /
  `print_quot_maps` inspection commands, and the tool-configuration commands