diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx index 440f51a1ab98d3357997e678ff3020885391cc8d..d219313e4cc1cd5aea8174b1ffcdcc0ac83af2a5 100644 --- a/ivette/src/frama-c/kernel/SourceCode.tsx +++ b/ivette/src/frama-c/kernel/SourceCode.tsx @@ -95,10 +95,10 @@ export default function SourceCode() { const [command] = Settings.useGlobalSettings(Preferences.EditorCommand); const launchEditor = () => { - const cmd = command.replace('\%s', file).replace('\%d', line.toString()); + const cmd = command.replace('%s', file).replace('%d', line.toString()); const args = cmd.split(' '); const prog = args.shift(); - if (prog) System.spawn(prog, args); + if (prog) System.spawn(prog, args).catch(/* TODO */); }; // Building the React component. diff --git a/ivette/src/ivette/prefs.tsx b/ivette/src/ivette/prefs.tsx index b4fd8e08190ddefcdbc0f9738a2a53e10e7ad367..ab9ece62a458305c6e99bd1c81f5719ad6259ada 100644 --- a/ivette/src/ivette/prefs.tsx +++ b/ivette/src/ivette/prefs.tsx @@ -131,16 +131,10 @@ export function useThemeButtons(props: ThemeProps): ThemeControls { // -------------------------------------------------------------------------- export const EditorCommand = - new Settings.GString('Editor.Command', 'emacs +\%d \%s'); + new Settings.GString('Editor.Command', 'emacs +%d %s'); export interface EditorCommandProps { command: Settings.GlobalSettings<string>; } -// function produceCommand(command: string, file: string, line: number): string { -// command.replace('\%s', file); -// command.replace('\%d', line.toString()); -// return ""; -// } - // -------------------------------------------------------------------------- diff --git a/ivette/src/renderer/Preferences.tsx b/ivette/src/renderer/Preferences.tsx index b6696ab22adf0897681c3da0fb88c4d8b6f828cd..70731ab3b779de8e1108240c0923732cec80546c 100644 --- a/ivette/src/renderer/Preferences.tsx +++ b/ivette/src/renderer/Preferences.tsx @@ -86,11 +86,11 @@ function ThemeFields(props: P.ThemeProps) { // -------------------------------------------------------------------------- // --- Editor Command Forms // -------------------------------------------------------------------------- -function EditorCommandFields(props : P.EditorCommandProps) { - const command = Forms.useDefined( - Forms.useValid(Settings.useGlobalSettings(props.command) +function EditorCommandFields(props: P.EditorCommandProps) { + const command = Forms.useDefined(Forms.useValid( + Settings.useGlobalSettings(props.command), )); - return (<Forms.TextCodeField state={command} label="Command"/>); + return (<Forms.TextCodeField state={command} label="Command" />); } // -------------------------------------------------------------------------- @@ -116,7 +116,7 @@ export default (() => ( /> </Forms.Section> <Forms.Section label="Editor Command" unfold> - <EditorCommandFields command={P.EditorCommand}/> + <EditorCommandFields command={P.EditorCommand} /> </Forms.Section> </Forms.Page> ));