Hi,
First of I really like the interactive documentation pop-ups that Verso provides for Lean code blocks on websites.
But I was wondering if there a configuration to limit the trigger area for the tactics state pop-up to just the checkbox.
Currently the whole line will trigger the tactics state pop-up, so it is not possible to view the documentation of the used tactics or theorems.
Hovering over intro show tactics state
Only when the proof state checkbox is ticked, and the proof state is unfolded, one can hover over the tactics and theorems to see their documentation.
Hovering over intro show its documentation, if tactics state is unfolded
Is there an option that limits the activation of the tactics state pop-up to the checkbox, so documentation pop-ups are viewable without unfolding the tactics state?
Hover over yellow region shows intro documentation, hover over green region shows tactics state
Hi,
First of I really like the interactive documentation pop-ups that Verso provides for Lean code blocks on websites.
But I was wondering if there a configuration to limit the trigger area for the tactics state pop-up to just the checkbox.
Currently the whole line will trigger the tactics state pop-up, so it is not possible to view the documentation of the used tactics or theorems.
Hovering over intro show tactics state
Only when the proof state checkbox is ticked, and the proof state is unfolded, one can hover over the tactics and theorems to see their documentation.
Hovering over intro show its documentation, if tactics state is unfolded
Is there an option that limits the activation of the tactics state pop-up to the checkbox, so documentation pop-ups are viewable without unfolding the tactics state?
Hover over yellow region shows intro documentation, hover over green region shows tactics state