Merge pull request #783 from ilesinge/hover_tooltip

Implement optional hover tooltip with function documentation
This commit is contained in:
Felix Roos 2023-11-05 22:10:25 +01:00 committed by GitHub
commit 62eb9ce598
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 90 additions and 2 deletions

View file

@ -385,6 +385,7 @@ function SettingsTab({ scheduler }) {
keybindings,
isLineNumbersDisplayed,
isAutoCompletionEnabled,
isTooltipEnabled,
isLineWrappingEnabled,
fontSize,
fontFamily,
@ -457,6 +458,11 @@ function SettingsTab({ scheduler }) {
onChange={(cbEvent) => settingsMap.setKey('isAutoCompletionEnabled', cbEvent.target.checked)}
value={isAutoCompletionEnabled}
/>
<Checkbox
label="Enable tooltips on Ctrl and hover"
onChange={(cbEvent) => settingsMap.setKey('isTooltipEnabled', cbEvent.target.checked)}
value={isTooltipEnabled}
/>
<Checkbox
label="Enable line wrapping"
onChange={(cbEvent) => settingsMap.setKey('isLineWrappingEnabled', cbEvent.target.checked)}

View file

@ -126,6 +126,7 @@ export function Repl({ embedded = false }) {
fontFamily,
isLineNumbersDisplayed,
isAutoCompletionEnabled,
isTooltipEnabled,
isLineWrappingEnabled,
panelPosition,
isZen,
@ -335,6 +336,7 @@ export function Repl({ embedded = false }) {
keybindings={keybindings}
isLineNumbersDisplayed={isLineNumbersDisplayed}
isAutoCompletionEnabled={isAutoCompletionEnabled}
isTooltipEnabled={isTooltipEnabled}
isLineWrappingEnabled={isLineWrappingEnabled}
fontSize={fontSize}
fontFamily={fontFamily}