search

monadius / vscode-hol-light

An extension for VS Code which provides support for HOL Light
MIT License
3 stars 0 forks source link

Highlights does not disappear if I have multiple opened editors #8

Closed aqjune closed 5 months ago

aqjune commented 5 months ago

scrshot

Hi, :)

I often open multiple files and send statements from either file to REPL. This often happens when one file needs another file & I need to edit both. The above example (screenshot) has two editors that are open: one for a.ml and another one for b.ml .

However, if I alternatively select & send statements to REPL, e.g., (1) one at a.ml, (2) one at b.ml, and then (3) another one at a.ml, the first highlight at a.ml does not disappear anymore.

What do you think about keeping one selection highlight per editor at maximum? I think that keeping the highlight of a.ml at step (2) is still great because it helps remember what I did on a.ml .

monadius commented 5 months ago

Highlighting is improved in the new version of the extension (1.2.0). The text is correctly highlighted for all text editors. Also, if there are multiple visible editors with the same text document, then the text is highlighted in all these editors.

I also added two new commands for highlighting:

  1. Remove Highlighting (Alt + D): removes highlighting in the active text document.
  2. Jump to Highlighted Text (Alt + J): moves the cursor to the end of a highlighted text.
aqjune commented 5 months ago

Thanks! It worked wonderfully :)