Highlighting group CornelisType only affects InfoWindow

[milaurila]

I am able to change the highlighting in the .agda file buffer of every group I've tried so far, except for CornelisType.
Overriding the settings of this group only changes the colors in the InfoWindow (see screenshot). I'd like these settings
to apply to the file buffer as well, is this possible?

I'm not sure of what parts of my setup are relevant, let me know and I'll provide.

[isovector]

Great color scheme :)

The buffer highlighting comes directly from Agda, so it's a bit hard to say why exactly you're not getting the results you'd like.

As an easy shortcut, you could try copying the colorscheme directly from Certainty by Construction:

https://github.com/isovector/certainty-by-construction/blob/5149d4dbede579599adc9833c1d10ec0f6e85a04/format/tex/agda.sty#L180-L214

If instead you'd like to actually diagnose the problem here, try adding the following code temporarily to your vimrc:

" Show syntax highlighting groups for word under cursor
nnoremap <F2> :call <SID>SynStack()<CR>
function! <SID>SynStack()
    if !exists("*synstack")
        return
    endif
    echo map(synstack(line('.'), col('.')), 'synIDattr(v:val, "name")')
endfunc

and then pressing F2 while your cursor is over the term you'd like to change the highlighting of. It should dump out the highlighting group it's a part of and let you know what exactly needs to change.

[milaurila]

Thanks for the actual color codes, that makes things easier!

I couldn't get your function to work but found that I can do :Inspect on words to get their groups. This returns the
expected groups for all terms in the file buffer except data types which gives No items found at position X,Y in buffer Z. Doing :Inspect on data types in the Info Window returns CornelisType.

[isovector]

That sounds like a bug in cornelis! Please let me know what version of Agda you're running and I'll look into it

…

On June 16, 2024 3:33:58 p.m. PDT, milaurila ***@***.***> wrote: Thanks for the actual color codes, that makes things easier! I couldn't get your function to work but found that I can do `:Inspect` on words to get their groups. This returns the expected groups for all terms in the file buffer except data types which gives `No items found at position X,Y in buffer Z`. Doing `:Inspect` on data types in the Info Window returns `CornelisType`. -- Reply to this email directly or view it on GitHub: #153 (comment) You are receiving this because you commented. Message ID: ***@***.***>

[milaurila]

I was running Agda 2.6.3. Now 2.6.4 and the problem persists.

[Soares]

I think the issue is that CornelisType is fully broken. The relevant agda property is called 'datatype', not 'type', so the syntax group either needs to be renamed to CornelisDatatype (in which case the magic of toAtomName will make everything work properly, as in this PR: #188) or some glue needs to be added to translate between the thing that agda calls "datatype" and the thing Cornelis is calling "type".