Skip to content
Snippets Groups Projects
Commit 5758c4ce authored by Maxime Jacquemin's avatar Maxime Jacquemin
Browse files

[ivette] Minor details

parent e99289d6
No related branches found
No related tags found
No related merge requests found
...@@ -1297,7 +1297,7 @@ export function MenuField<A>(props: MenuFieldProps<A>): JSX.Element { ...@@ -1297,7 +1297,7 @@ export function MenuField<A>(props: MenuFieldProps<A>): JSX.Element {
const entries: ENTRY<A>[] = React.useMemo(() => const entries: ENTRY<A>[] = React.useMemo(() =>
props.options.map((e, k) => { props.options.map((e, k) => {
const field = `item#${k}`; const field = `item#${k}`;
const option = <option value={field} label={e.label} />; const option = <option value={field} key={field} label={e.label} />;
return { field, option, value: e.value }; return { field, option, value: e.value };
}), [props.options]); }), [props.options]);
const input = React.useCallback( const input = React.useCallback(
......
...@@ -164,7 +164,7 @@ export default function ASTview() { ...@@ -164,7 +164,7 @@ export default function ASTview() {
const multipleSelections = selection?.multiple.allSelections; const multipleSelections = selection?.multiple.allSelections;
const theFunction = selection?.current?.fct; const theFunction = selection?.current?.fct;
const theMarker = selection?.current?.marker; const theMarker = selection?.current?.marker;
const { buttons: themeButtons, fontSize, wrapText } = const { buttons: editorButtons, fontSize, wrapText } =
Preferences.useEditorButtons({ Preferences.useEditorButtons({
fontSize: Preferences.AstFontSize, fontSize: Preferences.AstFontSize,
wrapText: Preferences.AstWrapText, wrapText: Preferences.AstWrapText,
...@@ -304,7 +304,7 @@ export default function ASTview() { ...@@ -304,7 +304,7 @@ export default function ASTview() {
return ( return (
<> <>
<TitleBar> <TitleBar>
{themeButtons} {editorButtons}
</TitleBar> </TitleBar>
<Text <Text
buffer={buffer} buffer={buffer}
......
...@@ -34,7 +34,6 @@ import * as Status from 'frama-c/kernel/Status'; ...@@ -34,7 +34,6 @@ import * as Status from 'frama-c/kernel/Status';
import * as States from 'frama-c/states'; import * as States from 'frama-c/states';
import * as PivotState from 'frama-c/plugins/pivot/api/general'; import * as PivotState from 'frama-c/plugins/pivot/api/general';
import PivotTableUI from 'react-pivottable/PivotTableUI'; import PivotTableUI from 'react-pivottable/PivotTableUI';
// import 'react-pivottable/pivottable.css';
import 'frama-c/kernel/PivotTable-style.css'; import 'frama-c/kernel/PivotTable-style.css';
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
......
...@@ -80,7 +80,7 @@ export default function SourceCode(): JSX.Element { ...@@ -80,7 +80,7 @@ export default function SourceCode(): JSX.Element {
const filename = Path.parse(file).base; const filename = Path.parse(file).base;
// Title bar buttons, along with the parameters for our text. // Title bar buttons, along with the parameters for our text.
const { buttons: themeButtons, fontSize, wrapText } = const { buttons: editorButtons, fontSize, wrapText } =
Preferences.useEditorButtons({ Preferences.useEditorButtons({
fontSize: Preferences.SourceFontSize, fontSize: Preferences.SourceFontSize,
wrapText: Preferences.AstWrapText, wrapText: Preferences.AstWrapText,
...@@ -196,7 +196,7 @@ export default function SourceCode(): JSX.Element { ...@@ -196,7 +196,7 @@ export default function SourceCode(): JSX.Element {
/> />
<Code title={file} style={{ padding: '5px' }}>{filename}</Code> <Code title={file} style={{ padding: '5px' }}>{filename}</Code>
<Hfill /> <Hfill />
{themeButtons} {editorButtons}
</TitleBar> </TitleBar>
<Text <Text
buffer={buffer} buffer={buffer}
......
...@@ -54,7 +54,7 @@ export function ThemeSwitch(): JSX.Element { ...@@ -54,7 +54,7 @@ export function ThemeSwitch(): JSX.Element {
const [theme, setTheme] = Themes.useColorTheme(); const [theme, setTheme] = Themes.useColorTheme();
const other = theme === 'dark' ? 'light' : 'dark'; const other = theme === 'dark' ? 'light' : 'dark';
const position = theme === 'dark' ? 'left' : 'right'; const position = theme === 'dark' ? 'left' : 'right';
const title = `Switch to ${other} theme (right-click for full choice)`; const title = `Switch to ${other} theme`;
const onChange = (): void => setTheme(other); const onChange = (): void => setTheme(other);
return ( return (
<Toolbar.Switch <Toolbar.Switch
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment