diff --git a/ivette/src/dome/renderer/text/editor.tsx b/ivette/src/dome/renderer/text/editor.tsx
index a7cf8b2a73eff7705cdf0be8a36e88fd3d4ea261..1ec627f1dbf071a1a91094919ab3c7bbef39da60 100644
--- a/ivette/src/dome/renderer/text/editor.tsx
+++ b/ivette/src/dome/renderer/text/editor.tsx
@@ -26,10 +26,10 @@ import { EditorState, StateField, Facet, Extension } from '@codemirror/state';
import { Annotation, Transaction, RangeSet } from '@codemirror/state';
import { EditorView, ViewPlugin, ViewUpdate } from '@codemirror/view';
+import { Decoration, DecorationSet } from '@codemirror/view';
import { DOMEventMap as EventMap } from '@codemirror/view';
import { GutterMarker, gutter } from '@codemirror/view';
-import { showTooltip, Tooltip } from '@codemirror/view';
-import { DecorationSet } from '@codemirror/view';
+import { Tooltip, showTooltip } from '@codemirror/view';
import { lineNumbers } from '@codemirror/view';
import { parser } from '@lezer/cpp';
@@ -51,9 +51,10 @@ export { RangeSet } from '@codemirror/state';
// -----------------------------------------------------------------------------
// Helper types definitions.
+export type View = EditorView | null;
export type Range = { from: number, to: number };
+export type Set<A> = (view: View, value: A) => void;
export type Get<A> = (state: EditorState | undefined) => A;
-export type Set<A> = (view: EditorView | null, value: A) => void;
export interface Data<A, S> { init: A, get: Get<A>, structure: S }
// Event handlers type definition.
@@ -94,6 +95,8 @@ export type Dict = Record<string, unknown>;
export type Dependency<A> = Field<A> | Aspect<A>;
export type Dependencies<I extends Dict> = { [K in keyof I]: Dependency<I[K]> };
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -104,15 +107,15 @@ export type Dependencies<I extends Dict> = { [K in keyof I]: Dependency<I[K]> };
type Dep<A> = Dependency<A>;
type Deps<I extends Dict> = Dependencies<I>;
type Combine<Output> = (l: readonly Output[]) => Output;
+type Mapper<I extends Dict, A> = (d: Dep<I[typeof k]>, k: string) => A;
+type Transform<I extends Dict> = Mapper<I, unknown>;
// Helper function used to map a function over Dependencies.
-type Mapper<I extends Dict, A> = (d: Dep<I[typeof k]>, k: string) => A;
function mapDict<I extends Dict, A>(deps: Deps<I>, fn: Mapper<I, A>): A[] {
return Object.keys(deps).map((k) => fn(deps[k], k));
}
// Helper function used to transfrom a Dependencies will keeping its structure.
-type Transform<I extends Dict> = (d: Dep<I[typeof k]>, k: string) => unknown;
function transformDict<I extends Dict>(deps: Deps<I>, tr: Transform<I>): Dict {
return Object.fromEntries(Object.keys(deps).map(k => [k, tr(deps[k], k)]));
}
@@ -134,6 +137,8 @@ function getExtension<A>(dep: Dependency<A>): Extension {
else return dep.structure.extension;
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -255,6 +260,8 @@ export function createEventHandler<I extends Dict>(
return enables.concat(EditorView.domEventHandlers(domEventHandlers));
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -294,14 +301,15 @@ export const LanguageHighlighter: Extension =
// -----------------------------------------------------------------------------
-// Standard extensions builders
+// Standard extensions and commands
// -----------------------------------------------------------------------------
+// Create a text field that updates the CodeMirror document when set.
export type ToString<A> = (text: A) => string;
export function createTextField<A>(init: A, toString: ToString<A>): Field<A> {
- const { get, set, structure } = createField<A>(init);
+ const field = createField<A>(init);
const useSet: Set<A> = (view, text) => {
- set(view, text);
+ field.set(view, text);
React.useEffect(() => {
const selection = { anchor: 0 };
const length = view?.state.doc.length;
@@ -309,9 +317,11 @@ export function createTextField<A>(init: A, toString: ToString<A>): Field<A> {
view?.dispatch({ changes, selection });
}, [view, text]);
};
- return { init, get, set: useSet, structure };
+ return { ...field, set: useSet };
}
+// An extension displaying line numbers in a gutter. Does not display anything
+// if the document is empty.
export const LineNumbers = createLineNumbers();
function createLineNumbers(): Extension {
return lineNumbers({
@@ -322,43 +332,59 @@ function createLineNumbers(): Extension {
});
}
+// An extension highlighting the active line.
+export const HighlightActiveLine = createHighlightActiveLine();
+function createHighlightActiveLine(): Extension {
+ const highlight = Decoration.line({ class: 'cm-active-line' });
+ return createDecorator({}, (_, state) => {
+ if (state.doc.length === 0) return RangeSet.empty;
+ const { from } = state.doc.lineAt(state.selection.main.from);
+ const deco = highlight.range(from, from);
+ return RangeSet.of(deco);
+ });
+}
+
+// An extension handling the folding of foldable nodes. For exemple, If used
+// with the language highlighter defined above, it will provides interactions
+// to fold comments only.
export const FoldGutter = createFoldGutter();
function createFoldGutter(): Extension {
return Language.foldGutter();
}
-export function foldAll(view: EditorView | null): void {
+// Folds all the foldable nodes of the given view.
+export function foldAll(view: View): void {
if (view !== null) Language.foldAll(view);
}
-export function unfoldAll(view: EditorView | null): void {
+// Unfolds all the foldable nodes of the given view.
+export function unfoldAll(view: View): void {
if (view !== null) Language.unfoldAll(view);
}
-export function createLineField(): Field<number> {
- const { get, set, structure } = createField(0);
- const useSet: Set<number> = (view, lineNum) => {
- set(view, lineNum);
- React.useEffect(() => {
- if ((view?.state.doc.lines ?? 0) < lineNum + 1) return;
- const { from } = view?.state.doc.line(lineNum + 1) ?? { from: 0 };
- view?.dispatch({ selection: { anchor: from }, scrollIntoView: true });
- }, [view, lineNum]);
- };
- return { init: 0, get, set: useSet, structure };
+// Move to the given line. The indexation starts at 1.
+export function selectLine(view: View, line: number): void {
+ if (!view || view.state.doc.lines < line) return;
+ const doc = view.state.doc;
+ const { from: here } = doc.lineAt(view.state.selection.main.from);
+ const { from: goto } = doc.line(Math.max(line, 1));
+ if (here === goto) return;
+ view.dispatch({ selection: { anchor: goto }, scrollIntoView: true });
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
// Editor component
// -----------------------------------------------------------------------------
-export interface Editor { view: EditorView | null; component: JSX.Element }
+export interface Editor { view: View; component: JSX.Element }
export function Editor(extensions: Extension[]): Editor {
const parent = React.useRef(null);
- const editor = React.useRef<EditorView | null>(null);
+ const editor = React.useRef<View>(null);
const component = <div className='cm-global-box' ref={parent} />;
React.useEffect(() => {
if (!parent.current) return;
diff --git a/ivette/src/dome/renderer/text/style.css b/ivette/src/dome/renderer/text/style.css
index 540eeb59e9b6eb6c2ddc8d63ea75fe1f6d381084..10b543a0f2b0b6487cfb2d9509c8f55b8f4b6834 100644
--- a/ivette/src/dome/renderer/text/style.css
+++ b/ivette/src/dome/renderer/text/style.css
@@ -188,4 +188,6 @@
.cm-number { color: var(--codemirror-number); }
.cm-keyword { color: var(--codemirror-keyword); }
+.cm-active-line { background-color: var(--background); }
+
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index 0b1dff582fc566c9d8c544c8dce9b762972a1faf..efd0eee30cd8a551e06b285e09778762fb5edb0d 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -66,6 +66,8 @@ function mapFilter<A, B>(xs: A[], fn: (x: A) => B | undefined): B[] {
return xs.map(fn).filter(isDef);
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -144,6 +146,8 @@ function coveringNode(tree: Tree, pos: number): Node | undefined {
return undefined;
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -162,6 +166,8 @@ const Tree = Editor.createAspect({ t: Text }, ({t}) => textToTree(t) ?? empty);
// tree, represented by the <Tree> aspect.
const Ranges = Editor.createAspect({ t: Tree }, ({ t }) => markersRanges(t));
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -198,6 +204,21 @@ function createMarkerUpdater(): Editor.Extension {
});
}
+// Scroll the selected marker into view if needed. Used for when the marker is
+// changed outside of this component.
+function scrollMarkerIntoView(view: Editor.View, marker: Marker): void {
+ if (!view || !marker) return;
+ const selection = view.state.selection.main;
+ const ranges = Ranges.get(view.state).get(marker) ?? [];
+ if (ranges.length === 0) return;
+ const exists = ranges.find((range) => range === selection);
+ if (exists) return;
+ const { from: anchor } = ranges[0];
+ view.dispatch({ selection: { anchor }, scrollIntoView: true });
+}
+
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -239,6 +260,8 @@ function createHoveredUpdater(): Editor.Extension {
});
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -259,6 +282,8 @@ function createCodeDecorator(): Editor.Extension {
});
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -284,6 +309,8 @@ function createDeadCodeDecorator(): Editor.Extension {
});
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -379,6 +406,8 @@ function createPropertiesGutter(): Editor.Extension {
});
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -417,6 +446,8 @@ async function studia(props: StudiaProps): Promise<StudiaInfos> {
return { name, title: '', locations: [], index: 0 };
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -480,6 +511,8 @@ function createContextMenuHandler(): Editor.Extension {
});
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -537,6 +570,8 @@ function createTaintTooltip(): Editor.Extension {
});
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -565,6 +600,8 @@ function useFctTaints(fct: Fct): Eva.LvalueTaints[] {
return States.useRequest(Eva.taintedLvalues, fct, { onError: [] }) ?? [];
}
+// -----------------------------------------------------------------------------
+
// -----------------------------------------------------------------------------
@@ -622,6 +659,7 @@ export default function ASTview(): JSX.Element {
Dead.set(view, useFctDead(fct));
Callers.set(view, useFctCallers(fct));
TaintedLvalues.set(view, useFctTaints(fct));
+ React.useEffect(() => scrollMarkerIntoView(view, marker), [view, marker]);
return (
<div style={{ height: '100%', fontSize: `${fontSize}px` }}>
@@ -648,4 +686,4 @@ export default function ASTview(): JSX.Element {
);
}
-// --------------------------------------------------------------------------
+// -----------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/kernel/SourceCode.tsx b/ivette/src/frama-c/kernel/SourceCode.tsx
index dd778977069d2102fb6161a98036b7eaa334edbf..0dd061bc82b85c7440a23bb23250b04a5596d3f8 100644
--- a/ivette/src/frama-c/kernel/SourceCode.tsx
+++ b/ivette/src/frama-c/kernel/SourceCode.tsx
@@ -20,226 +20,159 @@
/* */
/* ************************************************************************ */
-// --------------------------------------------------------------------------
-// --- Source Code
-// --------------------------------------------------------------------------
-
import React from 'react';
-import * as Server from 'frama-c/server';
-import * as States from 'frama-c/states';
+import * as Path from 'path';
import * as Dome from 'dome';
import * as System from 'dome/system';
-import { RichTextBuffer } from 'dome/text/buffers';
-import { Text } from 'dome/text/editors';
-import { TitleBar } from 'ivette';
-import * as Preferences from 'ivette/prefs';
-import { functions, markerInfo, getMarkerAt } from 'frama-c/kernel/api/ast';
-import { Code } from 'dome/controls/labels';
-import { Hfill } from 'dome/layout/boxes';
-import { IconButton } from 'dome/controls/buttons';
-import * as Path from 'path';
+import * as Boxes from 'dome/layout/boxes';
+import * as Editor from 'dome/text/editor';
+import * as Labels from 'dome/controls/labels';
import * as Settings from 'dome/data/settings';
+import * as Buttons from 'dome/controls/buttons';
+
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
import * as Status from 'frama-c/kernel/Status';
+import * as Ast from 'frama-c/kernel/api/ast';
-import { registerSandbox } from 'ivette';
+import * as Ivette from 'ivette';
+import * as Preferences from 'ivette/prefs';
-import CodeMirror from 'codemirror/lib/codemirror';
-import 'codemirror/addon/selection/active-line';
-import 'codemirror/addon/dialog/dialog.css';
-import 'codemirror/addon/search/search';
-import 'codemirror/addon/search/searchcursor';
-import * as Editor from 'dome/text/editor';
-// --------------------------------------------------------------------------
-// --- Pretty Printing (Browser Console)
-// --------------------------------------------------------------------------
+// -----------------------------------------------------------------------------
+// Utilitary types and functions
+// -----------------------------------------------------------------------------
-const D = new Dome.Debug('Source Code');
+// Recovering the cursor position as a line and a column.
+interface Position { line: number, column: number }
+function getCursorPosition(view: Editor.View): Position {
+ const pos = view?.state.selection.main;
+ if (!view || !pos) return { line: 1, column: 1 };
+ const line = view.state.doc.lineAt(pos.from).number;
+ const column = (pos.goalColumn ?? 0) + 1;
+ return { line, column };
+}
-// --------------------------------------------------------------------------
-// --- Source Code Printer
-// --------------------------------------------------------------------------
+// Error messages.
+function setError(text: string): void {
+ Status.setMessage({ text, kind: 'error' });
+}
-// The SourceCode component, producing the GUI part showing the source code
-// corresponding to the selected function.
-// export function SourceCodeOld(): JSX.Element {
-export default function SourceCode(): JSX.Element {
+// Function launching the external editor at the currently selected position.
+interface LaunchEditorProps { view: Editor.View, file: string, command: string }
+async function launchEditor(props: LaunchEditorProps): Promise<void> {
+ const { view, file, command } = props;
+ if (!view || file === '') return;
+ const { line: l, column: c } = getCursorPosition(view);
+ const args = command
+ .replace('%s', file)
+ .replace('%n', l.toString())
+ .replace('%c', c.toString())
+ .split(' ');
+ const prog = args.shift(); if (!prog) return;
+ const text = `An error has occured when opening the external editor ${prog}`;
+ System.spawn(prog, args).catch(() => setError(text));
+}
- // Hooks
- const [buffer] = React.useState(() => new RichTextBuffer());
- const [selection, updateSelection] = States.useSelection();
- const theFunction = selection?.current?.fct;
- const theMarker = selection?.current?.marker;
- const markersInfo = States.useSyncArray(markerInfo);
- const functionsData = States.useSyncArray(functions).getArray();
-
- // Retrieving the file name and the line number from the selection and the
- // synchronized tables.
- const sloc =
- (theMarker && markersInfo.getData(theMarker)?.sloc) ??
- (theFunction && functionsData.find((e) => e.name === theFunction)?.sloc);
- const file = sloc ? sloc.file : '';
- const line = sloc ? sloc.line : 0;
- const filename = Path.parse(file).base;
+// -----------------------------------------------------------------------------
- // Global Font Size
- const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
- // Updating the buffer content.
- const text = React.useMemo(async () => {
- const onError = (): string => {
- if (file)
- D.error(`Fail to load source code file ${file}`);
- return '';
- };
- return System.readFile(file).catch(onError);
- }, [file]);
- const { result } = Dome.usePromise(text);
- React.useEffect(() => buffer.setValue(result), [buffer, result]);
-
- /* Last location selected by a click in the source code. */
- const selected: React.MutableRefObject<undefined | States.Location> =
- React.useRef();
-
- /* Updates the cursor position according to the current [selection], except
- when the [selection] is changed according to a click in the source code,
- in which case the cursor should stay exactly where the user clicked. */
- React.useEffect(() => {
- if (selected.current && selected?.current === selection?.current)
- selected.current = undefined;
- else
- buffer.setCursorOnTop(line);
- }, [buffer, selection, line, result]);
-
- /* CodeMirror types used to bind callbacks to extraKeys. */
- type position = CodeMirror.Position;
- type editor = CodeMirror.Editor;
-
- const selectCallback = React.useCallback(
- async function select(editor: editor, event: MouseEvent) {
- const pos = editor.coordsChar({ left: event.x, top: event.y });
- if (file === '' || !pos) return;
- const arg = [file, pos.line + 1, pos.ch + 1];
- Server
- .send(getMarkerAt, arg)
- .then(([fct, marker]) => {
- if (fct || marker) {
- const location = { fct, marker } as States.Location;
- selected.current = location;
- updateSelection({ location });
- }
- })
- .catch((err) => {
- D.error(`Failed to get marker from source file position: ${err}`);
- Status.setMessage({
- text: 'Failed request to Frama-C server',
- kind: 'error',
- });
- });
- },
- [file, updateSelection],
- );
- React.useEffect(() => {
- buffer.forEach((cm) => cm.on('mousedown', selectCallback));
- return () => buffer.forEach((cm) => cm.off('mousedown', selectCallback));
- }, [buffer, selectCallback]);
+// -----------------------------------------------------------------------------
+// Fields declarations
+// -----------------------------------------------------------------------------
- const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
- async function launchEditor(_?: editor, pos?: position): Promise<void> {
- if (file !== '') {
- const selectedLine = pos ? (pos.line + 1).toString() : '1';
- const selectedChar = pos ? (pos.ch + 1).toString() : '1';
- const cmd = command
- .replace('%s', file)
- .replace('%n', selectedLine)
- .replace('%c', selectedChar);
- const args = cmd.split(' ');
- const prog = args.shift();
- if (prog) System.spawn(prog, args).catch(() => {
- Status.setMessage({
- text: `An error has occured when opening the external editor ${prog}`,
- kind: 'error',
- });
- });
- }
- }
-
- async function contextMenu(editor?: editor, pos?: position): Promise<void> {
- if (file !== '') {
- const items = [
- {
- label: 'Open file in an external editor',
- onClick: () => launchEditor(editor, pos),
- },
- ];
- Dome.popupMenu(items);
- }
- }
+// The Ivette selection must be updated by the CodeMirror plugin. This field
+// adds the callback in the CodeMirror internal state.
+type UpdateSelection = (a: States.SelectionActions) => void;
+const UpdateSelection = Editor.createField<UpdateSelection>(() => { return; });
- const externalEditorTitle =
- 'Open the source file in an external editor.\nA Ctrl-click '
- + 'in the source code opens the editor at the selected location.'
- + '\nThe editor used can be configured in Ivette settings.';
+// Those fields contain the source code and the file name.
+const Source = Editor.createTextField<string>('', (s) => s);
+const File = Editor.createField<string>('');
+
+// const Line = Editor.createLineField();
+
+// This field contains the command use to start the external editor.
+const Command = Editor.createField<string>('');
+
+// -----------------------------------------------------------------------------
- // Building the React component.
- return (
- <>
- <TitleBar>
- <IconButton
- icon="DUPLICATE"
- visible={file !== ''}
- onClick={launchEditor}
- title={externalEditorTitle}
- />
- <Code title={file}>{filename}</Code>
- <Hfill />
- </TitleBar>
- <Text
- buffer={buffer}
- mode="text/x-csrc"
- fontSize={fontSize}
- selection={theMarker}
- lineNumbers={!!theFunction}
- styleActiveLine={!!theFunction}
- extraKeys={{
- 'Alt-F': 'findPersistent',
- 'Ctrl-LeftClick': launchEditor as (_: CodeMirror.Editor) => void,
- RightClick: contextMenu as (_: CodeMirror.Editor) => void,
- }}
- readOnly
- />
- </>
- );
+
+// -----------------------------------------------------------------------------
+// Context menu and source interactions
+// -----------------------------------------------------------------------------
+
+// This events handler takes care of the context menu, of the selection in the
+// source code (updating the global Ivette's selection) and of the meta
+// selection (with the ctrl modificator) to launch the external editor.
+const EventsHandler = createEventsHandler();
+function createEventsHandler(): Editor.Extension {
+ const deps = { file: File, command: Command, update: UpdateSelection };
+ return Editor.createEventHandler(deps, {
+ contextmenu: ({ file, command }, view) => {
+ if (file === '') return;
+ const launch = (): Promise<void> => launchEditor({ view, file, command });
+ const label = 'Open file in an external editor';
+ Dome.popupMenu([ { label, onClick: launch } ]);
+ },
+ mouseup: ({ file, command, update }, view, event) => {
+ if (file === '') return;
+ const { line, column } = getCursorPosition(view);
+ Server
+ .send(Ast.getMarkerAt, [file, line, column])
+ .then(([fct, marker]) => {
+ if (fct || marker) update({ location: { fct, marker } });
+ })
+ .catch(() => setError('Failed to request to Frama-C server'));
+ if (event.ctrlKey) launchEditor({ view, file, command });
+ },
+ });
}
-// --------------------------------------------------------------------------
+// -----------------------------------------------------------------------------
+
-const Source = Editor.createTextField<string>('', (s) => s);
-const Line = Editor.createLineField();
+// -----------------------------------------------------------------------------
+// Server requests
+// -----------------------------------------------------------------------------
+
+// Server request handler returning the source code.
function useFctSource(file: string): string {
const req = React.useMemo(() => System.readFile(file), [file]);
const { result } = Dome.usePromise(req);
return result ?? '';
}
+// -----------------------------------------------------------------------------
+
+
+
+// -----------------------------------------------------------------------------
+// Source Code component
+// -----------------------------------------------------------------------------
+
+// Necessary extensions.
const baseExtensions: Editor.Extension[] = [
Source.structure,
- Line.structure,
Editor.LineNumbers,
Editor.LanguageHighlighter,
+ Editor.HighlightActiveLine,
+ EventsHandler,
];
-export function SourceCodeNew(): JSX.Element {
-// export default function SourceCode(): JSX.Element {
+// The component in itself.
+export default function SourceCode(): JSX.Element {
+ const [fontSize] = Settings.useGlobalSettings(Preferences.EditorFontSize);
+ const [command] = Settings.useGlobalSettings(Preferences.EditorCommand);
const { view, component } = Editor.Editor(baseExtensions);
- const functionsData = States.useSyncArray(functions).getArray();
- const markersInfo = States.useSyncArray(markerInfo);
- const [selection] = States.useSelection();
+ const functionsData = States.useSyncArray(Ast.functions).getArray();
+ const markersInfo = States.useSyncArray(Ast.markerInfo);
+ const [selection, updateSelection] = States.useSelection();
const marker = selection?.current?.marker;
const fct = selection?.current?.fct;
@@ -248,14 +181,34 @@ export function SourceCodeNew(): JSX.Element {
const sloc = markerSloc ?? fctSloc;
const file = sloc ? sloc.file : '';
const line = sloc ? sloc.line : 0;
+ const filename = Path.parse(file).base;
Source.set(view, useFctSource(file));
- Line.set(view, line);
- return component;
+ UpdateSelection.set(view, updateSelection);
+ Command.set(view, command);
+ File.set(view, file);
+ Editor.selectLine(view, line);
+
+ const externalEditorTitle =
+ 'Open the source file in an external editor.\nA Ctrl-click '
+ + 'in the source code opens the editor at the selected location.'
+ + '\nThe editor used can be configured in Ivette settings.';
+
+ return (
+ <div style={{ height: '100%', fontSize: `${fontSize}px` }}>
+ <Ivette.TitleBar>
+ <Buttons.IconButton
+ icon="DUPLICATE"
+ visible={file !== ''}
+ onClick={() => launchEditor({ view, file, command })}
+ title={externalEditorTitle}
+ />
+ <Labels.Code title={file}>{filename}</Labels.Code>
+ <Boxes.Hfill />
+ </Ivette.TitleBar>
+ {component}
+ </div>
+ );
}
-registerSandbox({
- id: 'sandbox.sourceCode',
- label: 'SourceCode CodeMirror6',
- children: <SourceCodeNew />,
-});
+// -----------------------------------------------------------------------------