feat(theme): add the four Lean 4 capture entries (Arc 8 Stage 1, Q#LN4)
`constructor`, `character`, `keyword.conditional`, and `warning` are the captures the Lean query uses that the global theme table lacked. Three of them are not Lean-only, so this is a deliberate retro-paint of already shipped languages -- the #146 lesson applied on purpose rather than discovered afterwards. The blast radius, measured rather than assumed: * `constructor` reaches SEVEN language entries, not four. The emitting crates are rust, lua, python and javascript, but `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated base-first into javascriptreact, typescript and typescriptreact as well. * Its shape is not "constructors". rust/python/javascript tag every capitalized identifier (`#match? "^[A-Z]"`); lua tags every table-constructor brace. So this recolors `None`, every class-cased name, and every Lua `{}` -- all of which rendered as unstyled default text before. * `character` reaches zig only; `keyword.conditional` reaches cmake and zig, which previously flattened it to `keyword`; `warning` reaches no other grammar and exists for Lean's `sorry`. The alternative was an in-repo overlay renaming the captures (the #144 LaTeX pattern), which forks a 213-line query we would then own and hand-merge on every crate bump. There is no middle option: styling Lean's constructors without touching the other seven entries requires renaming the capture, which requires the overlay. Pinned in both directions, per #146: * the positive breadth pin asserts all seven entries emit `@constructor` at the QUERY level -- chosen over per-fixture checks because the base-query composition is the fragile part; if someone stops concatenating the JS base into `typescript`, this fails while any single-language fixture still passes; * two grid pins prove the theme entry reaches painted cells, and a third records that a variant in CALL position keeps `@function` -- the difference between "capitalized identifiers recolor" and "enum variants recolor", only the first of which is true; * the negative pin asserts ten languages (markdown, json, yaml, html, css, c, cpp, go, toml, bash) emit none of the four names, with a non-vacuity check that the same predicate finds each name where it does occur. Rev 1 of the framing named Lua and Python in that negative pin, which was a self-contradiction -- both are retro-painted by `constructor`, so the assertion would have been vacuous in the #155 R2 shape. Review round 1 caught it. Full lib suite (1,824) and the required-GPU gate (152) pass unchanged, so no existing assertion depended on these captures being unstyled. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This commit is contained in:
parent
6ea8d2756e
commit
5207d40caf
193
src/highlight.rs
193
src/highlight.rs
|
|
@ -174,6 +174,41 @@ impl Theme {
|
|||
// prefix-walks to `tag`.
|
||||
("tag", fg(5)),
|
||||
("attribute", fg(3)),
|
||||
// Lean 4 (framing Q#LN4). These four are the captures the Lean
|
||||
// query uses that the set above lacks — but three of them are
|
||||
// NOT Lean-only, and adding them here changes languages that
|
||||
// already ship. That is the #146 lesson (`attribute`, above,
|
||||
// retro-painted rust/lua/yaml) and it is deliberate, not
|
||||
// incidental:
|
||||
//
|
||||
// * `constructor` reaches SEVEN entries — rust, lua, python,
|
||||
// javascript, and (because `tree_sitter_javascript::
|
||||
// HIGHLIGHT_QUERY` is concatenated base-first into them)
|
||||
// javascriptreact, typescript, typescriptreact. Its shape is
|
||||
// not "constructors": rust/python/javascript tag every
|
||||
// capitalized identifier (`#match? "^[A-Z]"`), and lua tags
|
||||
// every table-constructor brace. So this recolors `Some`,
|
||||
// `None`, `Ok`, `Err`, every class-cased name, and every Lua
|
||||
// `{}`. All of those render as unstyled default text today.
|
||||
// * `character` reaches zig only.
|
||||
// * `keyword.conditional` reaches cmake and zig, which
|
||||
// currently flatten it to `keyword`; giving it
|
||||
// `keyword.control`'s style makes their conditionals read the
|
||||
// way rust's already do.
|
||||
// * `warning` reaches no other grammar. It exists for Lean's
|
||||
// `sorry` — an unproved goal, the single most important thing
|
||||
// to see in a proof file.
|
||||
//
|
||||
// The alternative was an in-repo query overlay renaming these
|
||||
// into the existing vocabulary (the #144 LaTeX pattern), which
|
||||
// would fork a 213-line query we would then own and hand-merge
|
||||
// on every crate bump. There is no middle option: styling Lean's
|
||||
// constructors without touching the other seven entries requires
|
||||
// renaming the capture, which requires the overlay.
|
||||
("constructor", fg(11)),
|
||||
("character", fg(2)),
|
||||
("keyword.conditional", fg_bold(13)),
|
||||
("warning", fg_bold(1)),
|
||||
];
|
||||
let by_capture = entries
|
||||
.iter()
|
||||
|
|
@ -1484,6 +1519,164 @@ mod tests {
|
|||
);
|
||||
}
|
||||
|
||||
/// Paint `src` as `language` into a one-row grid and return the style
|
||||
/// at column `col`. Shared by the Q#LN4 retro-paint pins below.
|
||||
fn painted_fg_at(
|
||||
language_name: &str,
|
||||
file: &str,
|
||||
src: &str,
|
||||
col: u32,
|
||||
) -> pmacs_protocol::cell::Color {
|
||||
use crate::buffer::{Buffer, BufferId, EditOp};
|
||||
use crate::cell::{Cell, CellSize};
|
||||
use crate::syntax::{ParseView, SyntaxRegistry};
|
||||
|
||||
let reg = SyntaxRegistry::new();
|
||||
let language = reg.language(language_name).expect("grammar loads");
|
||||
let mut buf = Buffer::new(BufferId::next(), file);
|
||||
buf.apply_edit(EditOp::Insert {
|
||||
pos: 0,
|
||||
bytes: src.as_bytes(),
|
||||
})
|
||||
.unwrap();
|
||||
let view = ParseView::new(&buf, language, language_name.to_owned());
|
||||
let handle = view.handle();
|
||||
let _vid = buf.attach_view(Box::new(view));
|
||||
let mut req = handle.make_request();
|
||||
req.injection_aliases = reg.injection_alias_snapshot();
|
||||
let bundle = crate::syntax::run_parse(req).expect("parse");
|
||||
handle.install(reg.resolve_layer_queries(&bundle));
|
||||
|
||||
let mut hv = SyntaxHighlightView::new(handle, reg.theme());
|
||||
let (rows, cols) = (1usize, 40usize);
|
||||
let mut backing: Vec<Cell> = vec![Cell::default(); rows * cols];
|
||||
let mut grid = CellGrid {
|
||||
cells: &mut backing,
|
||||
stride: cols as u32,
|
||||
size: CellSize::new(rows as u32, cols as u32),
|
||||
};
|
||||
let viewport = Viewport {
|
||||
buffer_start: 0,
|
||||
buffer_end: u64::MAX,
|
||||
cell_origin: CellCoord::new(0, 0),
|
||||
cell_size: CellSize::new(rows as u32, cols as u32),
|
||||
gutter_w: 0,
|
||||
folds: None,
|
||||
};
|
||||
hv.render(&buf, viewport, &mut grid);
|
||||
grid.get(CellCoord::new(0, col)).style.fg
|
||||
}
|
||||
|
||||
/// Does `language`'s compiled highlight query use `capture`?
|
||||
fn query_uses_capture(language: &str, capture: &str) -> bool {
|
||||
let reg = crate::syntax::SyntaxRegistry::new();
|
||||
let Some(query) = reg.highlights_query(language) else {
|
||||
panic!("{language} has no highlights query");
|
||||
};
|
||||
query.capture_names().contains(&capture)
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn lean4_constructor_capture_retro_paints_the_whole_javascript_family() {
|
||||
// Framing acceptance 7 (Q#LN4), the breadth half. `constructor` was
|
||||
// added for Lean, but four crates emit it — and because
|
||||
// `tree_sitter_javascript::HIGHLIGHT_QUERY` is concatenated
|
||||
// base-first into the react/typescript entries
|
||||
// (`src/syntax.rs`), it reaches SEVEN language entries, not four.
|
||||
//
|
||||
// Asserted at the query level rather than per-fixture precisely
|
||||
// because the composition is the fragile part: if someone stops
|
||||
// concatenating the JS base query into `typescript`, this fails
|
||||
// while any single-language fixture would still pass.
|
||||
for language in [
|
||||
"rust",
|
||||
"lua",
|
||||
"python",
|
||||
"javascript",
|
||||
"javascriptreact",
|
||||
"typescript",
|
||||
"typescriptreact",
|
||||
] {
|
||||
assert!(
|
||||
query_uses_capture(language, "constructor"),
|
||||
"`{language}` emits @constructor, so Q#LN4's entry retro-paints it"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn lean4_capture_additions_paint_rust_constructors_and_lua_braces() {
|
||||
// Framing acceptance 7, the "actually reaches painted cells" half —
|
||||
// a query-name check alone would not prove the theme entry resolves.
|
||||
// Both of these rendered as unstyled default text before Q#LN4.
|
||||
use pmacs_protocol::cell::Color;
|
||||
|
||||
// `None` at col 8 — a bare capitalized identifier, which is what the
|
||||
// rust query's `#match? "^[A-Z]"` tags. Note that `Some(1)` does NOT
|
||||
// work here: in call position a narrower `@function` pattern wins and
|
||||
// paints fg 4. The distinction is worth keeping in the test, because
|
||||
// it is the difference between "capitalized identifiers recolor" and
|
||||
// "enum variants recolor" — only the former is true.
|
||||
assert_eq!(
|
||||
painted_fg_at("rust", "a.rs", "let x = None;\n", 8),
|
||||
Color::Indexed(11),
|
||||
"a bare Rust capitalized identifier paints the shared @constructor style"
|
||||
);
|
||||
// `Some` in pattern position (col 10) does reach @constructor.
|
||||
assert_eq!(
|
||||
painted_fg_at("rust", "a.rs", "match v { Some(z) => z, None => 0 };\n", 10),
|
||||
Color::Indexed(11),
|
||||
"a Rust pattern-position variant paints the shared @constructor style"
|
||||
);
|
||||
// ...but in CALL position the narrower @function pattern wins. Pinned
|
||||
// so the blast radius recorded in the framing stays accurate.
|
||||
assert_eq!(
|
||||
painted_fg_at("rust", "a.rs", "let e = Err(1);\n", 8),
|
||||
Color::Indexed(4),
|
||||
"a called variant keeps @function, not @constructor"
|
||||
);
|
||||
// Lua tags the table-constructor BRACES, not a name: `{` at col 8.
|
||||
assert_eq!(
|
||||
painted_fg_at("lua", "a.lua", "local t = {}\n", 10),
|
||||
Color::Indexed(11),
|
||||
"a Lua table brace paints the shared @constructor style"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn lean4_capture_additions_do_not_reach_unrelated_languages() {
|
||||
// Framing acceptance 8 — the negative pin, redrawn in review round 1.
|
||||
//
|
||||
// Rev 1 named Lua and Python here, which was a self-contradiction:
|
||||
// both are retro-painted by `constructor`, so a "nothing moved"
|
||||
// assertion over them would have been vacuous — the #155 R2 shape.
|
||||
// These ten emit NONE of the four names, verified by grep over the
|
||||
// crate queries in the dependency graph.
|
||||
//
|
||||
// Stated at the query level, which is stronger than a fixture
|
||||
// snapshot: it holds for every construct in the language, not just
|
||||
// the one a fixture happened to exercise.
|
||||
const ADDED: [&str; 4] = ["constructor", "character", "keyword.conditional", "warning"];
|
||||
for language in [
|
||||
"markdown", "json", "yaml", "html", "css", "c", "cpp", "go", "toml", "bash",
|
||||
] {
|
||||
for capture in ADDED {
|
||||
assert!(
|
||||
!query_uses_capture(language, capture),
|
||||
"`{language}` must not emit @{capture}; Q#LN4 would silently restyle it"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
// Non-vacuity: the same predicate must find each name where it DOES
|
||||
// occur. Without this, a `query_uses_capture` that always returned
|
||||
// false would pass the loop above.
|
||||
assert!(query_uses_capture("lean4", "constructor"));
|
||||
assert!(query_uses_capture("zig", "character"));
|
||||
assert!(query_uses_capture("cmake", "keyword.conditional"));
|
||||
assert!(query_uses_capture("lean4", "warning"));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn web_grid_paints_html_tag_and_attribute() {
|
||||
// Q#WEB4 acceptance: the two capture entries this lane adds (`tag`,
|
||||
|
|
|
|||
Loading…
Reference in New Issue