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: https://github.com/isovector/cornelis/issues/153#issuecomment-2171914454 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.