diff --git a/ivette/.dome-pkg-app.lock b/ivette/.dome-pkg-app.lock
index 6db93f438a0241f68348c0d419b47d9bc13ebfd5..694887d64d5abc25568980ca5583c522b08b8e33 100644
--- a/ivette/.dome-pkg-app.lock
+++ b/ivette/.dome-pkg-app.lock
@@ -1 +1 @@
-react@^16 react-dom@^16 source-map-support lodash react-virtualized react-draggable react-fast-compare codemirror@^5 diff
+react@^16 react-dom@^16 source-map-support lodash react-virtualized react-draggable react-fast-compare diff
diff --git a/ivette/package.json b/ivette/package.json
index 00f9db30760ad478740809f246da7867c4bfb7c0..76100c824ae8078168af3a968d0fe58212e813c2 100644
--- a/ivette/package.json
+++ b/ivette/package.json
@@ -73,7 +73,6 @@
"@fortawesome/fontawesome-free": "",
"@types/diff": "",
"@types/react-window": "",
- "codemirror": "^5",
"cytoscape": "",
"cytoscape-cola": "",
"cytoscape-cose-bilkent": "",
@@ -82,7 +81,7 @@
"cytoscape-klay": "",
"cytoscape-panzoom": "",
"cytoscape-popper": "",
- "diff": "",
+ "diff": "^5.1.0",
"gremlins.js": "^2.2.0",
"immutable": "",
"jsdiff": "^1.1.1",
diff --git a/ivette/src/dome/renderer/text/buffers.ts b/ivette/src/dome/renderer/text/buffers.ts
deleted file mode 100644
index 249f2a81ea8d5ec04c1ab5a638210358a6327d2a..0000000000000000000000000000000000000000
--- a/ivette/src/dome/renderer/text/buffers.ts
+++ /dev/null
@@ -1,687 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2023 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/* ************************************************************************ */
-
-/* eslint-disable @typescript-eslint/no-explicit-any */
-
-// --------------------------------------------------------------------------
-// --- Text Documents
-// --------------------------------------------------------------------------
-
-/**
- @packageDocumentation
- @module dome/text/buffers
-*/
-
-import Emitter from 'events';
-import CodeMirror from 'codemirror/lib/codemirror';
-import { Debug } from 'dome';
-
-const D = new Debug('Dome.text');
-
-export type Range = { from: CodeMirror.Position; to: CodeMirror.Position };
-
-export interface Decorator {
- /** @return a className to apply on markers with the identifier. */
- (id: string): string | undefined;
-}
-
-export interface TextMarkerProxy {
- clear(): void;
- changed(): void;
- find(): Range | undefined;
-}
-
-/**
- Text Marker options.
-
- Inherits CodeMirror
- [TextMerkerOptions](https://codemirror.net/doc/manual.html#api_marker).
- */
-export interface MarkerProps extends CodeMirror.TextMarkerOptions {
- id?: string;
- hover?: boolean;
- className?: string;
-}
-
-export interface CSSMarker {
- /** Hover class `'dome-xHover-nnn'` */
- classNameId: string;
- /** Marker id */
- id: string | undefined;
- /** Hovered marker */
- hover: boolean;
- /** Size in character */
- length: number;
-}
-
-// --------------------------------------------------------------------------
-// --- Batched Update
-// --------------------------------------------------------------------------
-
-const BATCH_OPS = 500;
-const BATCH_DELAY = 5;
-const BATCH_RMAX = 1000; // max tag range for sorting
-const BATCH_MARGINS = 20; // visible lines above the viewport
-
-interface MarkerOptions {
- id?: string;
- hover?: boolean;
- className?: string;
- options: CodeMirror.TextMarkerOptions;
-}
-
-interface StackedMarker extends MarkerOptions {
- startIndex: number;
-}
-
-interface BufferedMarker extends MarkerOptions {
- startIndex: number;
- stopIndex: number;
-}
-
-type BufferedTag = BufferedMarker | undefined;
-
-function rankTag(lmin: number, lmax: number, tg: BufferedTag): number {
- if (tg && (lmin <= tg.stopIndex || tg.startIndex <= lmax)) {
- const size = tg.stopIndex - tg.startIndex;
- return size < BATCH_RMAX ? size : BATCH_RMAX;
- }
- return BATCH_RMAX;
-}
-
-const byVisibleTag =
- (lmin: number, lmax: number) =>
- (a: BufferedTag, b: BufferedTag): number => (
- rankTag(lmin, lmax, a) - rankTag(lmin, lmax, b)
- );
-
-// --------------------------------------------------------------------------
-// --- Buffer
-// --------------------------------------------------------------------------
-
-export type TextMarker = CodeMirror.TextMarker<CodeMirror.MarkerRange>;
-
-export interface RichTextBufferProps {
-
- /**
- * CodeMirror [mode](https://codemirror.net/mode/index.html) specification.
- */
- mode?: any;
-
- /** Maximum number of lines in the buffer. */
- maxlines?: number;
-
-}
-
-/**
- Rich Text Content and State.
-
- A buffer encapsulate a CodeMirror document instance inside an standard
- Node event emitter. CodeMirror signals are automatically linked back to
- the event emitter (on a lazy basis).
-
- All buffer modifications are stacked and executed asynchronously inside
- CodeMirror batched operations to increase performance.
-
- The `maxlines` will control the maximum number of lines kept in the buffer.
- By default, it is set to `10000`, but you can use `null`, `0` or any negative
- value to disable this behavior. See also `this.setMaxlines()` method.
-
- Additionnaly, a Buffer maintains an _edited_ state internally that can
- be manually updated, and that is automatically set to `true` when the
- underlying CodeMirror document is changed. It is associated to an `'edited'`
- event of the buffer, and can be used to manage the « Saved » / « Not-Saved »
- state of an editor, for instance.
-
- Typically, a sequence of changed events would fire a unique `'edited'` buffer
- event, untill `setEdited(false)` is invoked. The `clear()` method also resets
- the _edited_ state to `false`, but sill emit an `'edited'` event if the
- buffer was not empty.
-
- Buffers can also be updated programmatically by various methods. In addition
- to specified CodeMirror modes, you can also attach text markers
- programmatically with a push/pop API.
-
- Text markers can be associated with an identifier, that can be used for
- dynamic highlighting, called Decorations. Decorations are class names that
- add styling attributes upon the current mode. Typically, consider only using
- background colors, underlines and/or strike-through for decorations, since
- font styles and colors are likely to be managed by CodeMirror modes, unless
- you know exactly what your are doing.
-
- The `setDecorator` method can be used to set or update
- the highlighting function that computes the decoration of a text marker
- from its identifier. When the decorations may have change, you shall either
- set again the highlighting function with a call to `setDecorator()` or call
- the `updateDecorations()` method. This also triggers the `'decorated'` event.
-
- */
-
-export class RichTextBuffer extends Emitter {
-
- private document: CodeMirror.Doc;
- private maxlines = 10000;
- private editors: CodeMirror.Editor[] = [];
- private cacheIndex = 0; // document index, negative if not computed
- private bufferedText: string; // buffered text to append
- private bufferedTags: BufferedTag[];
- private stacked: StackedMarker[] = [];
- private batched = false;
-
- // Indexed by CSS property dome-xHover-nnnn
- private cssmarkers = new Map<string, CSSMarker>();
-
- // Indexed by marker user identifier
- private textmarkers = new Map<string, TextMarker[]>();
-
- private decorator?: Decorator;
- private edited = false;
- private focused = false;
- private markid = 0;
-
- constructor(props: RichTextBufferProps = {}) {
- super();
- const { mode, maxlines } = props;
- this.document = new CodeMirror.Doc('', mode);
- this.cacheIndex = -1;
- this.bufferedTags = [];
- this.bufferedText = '';
- this.setMaxlines(maxlines);
- this.setEdited = this.setEdited.bind(this);
- this.setFocused = this.setFocused.bind(this);
- this.clear = this.clear.bind(this);
- this.append = this.append.bind(this);
- this.setValue = this.setValue.bind(this);
- this.getValue = this.getValue.bind(this);
- this.updateDecorations = this.updateDecorations.bind(this);
- this.onChange = this.onChange.bind(this);
- this.doBatch = this.doBatch.bind(this);
- this.log = this.log.bind(this);
- }
-
- /**
- Internal CodeMirror
- [document](https://codemirror.net/doc/manual.html#api_doc) instance.
- */
- getDoc(): CodeMirror.Doc { return this.document; }
-
- // --------------------------------------------------------------------------
- // --- Buffer Manipulation
- // --------------------------------------------------------------------------
-
- /** Clear buffer contents and resets _edited_ state. */
- clear(): void { this.setValue(''); }
-
- /**
- Writes in the buffer. All parameters are converted to string and joined
- with spaces. The generated change event has origin `'buffer'` and it does
- not modifies the _edited_ internal state.
- */
- append(...values: any[]): void {
- if (values.length > 0) {
- const text = values.join(' ');
- this.bufferedText += text;
- this.armBatch();
- }
- }
-
- /**
- Starts a new line in the buffer. If the current buffer content does not
- finish at the beginning of a fresh line, inserts a newline character.
- */
- flushline(): void {
- const doc = this.document;
- const buf = this.bufferedText;
- if (buf === '') {
- const start = doc.posFromIndex(Infinity);
- if (start.ch > 0) doc.replaceRange('\n', start, undefined, 'buffer');
- this.cacheIndex = -1;
- } else if (buf[buf.length - 1] !== '\n') this.bufferedText += '\n';
- }
-
- /**
- Appends with newline and auto-scrolling. This is a short-cut to
- `flushline()` followed by `append(...value,'\n')` and `scroll()`.
- */
- log(...values: any[]): void {
- this.flushline();
- this.append(...values, '\n');
- this.scroll();
- }
-
- /**
- Replace all textual content with the given string.
- Also remove all markers.
- */
- setValue(txt = ''): void {
- this.document.setValue(txt);
- this.cssmarkers.clear();
- this.textmarkers.clear();
- this.stacked = [];
- this.bufferedTags = [];
- this.bufferedText = '';
- this.cacheIndex = 0;
- this.edited = false;
- this.focused = false;
- this.markid = 0;
- }
-
- /** Return the textual contents of the buffer. */
- getValue(): string { return this.document.getValue(); }
-
- // --------------------------------------------------------------------------
- // --- Text Markers
- // --------------------------------------------------------------------------
-
- /**
- Opens a text marker.
-
- Opens a text marker at the current (end) position in the buffer.
-
- The text marker is stacked and would be actually created on the matching
- [[closeTextMarker]] call. It will be applied to the full range of text
- inserted between its associated [[openTextMarker]] and [[closeTextMarker]]
- calls.
-
- The returned text marker is actually a _proxy_ to the text marker that will
- be eventually created by [[closeTextMarker]]. Its methods are automatically
- forwarded to the actual `CodeMirror.TextMarker` instance, once created.
- Hence, you can safely invoke these methods on either the _proxy_ or the
- _final_ text marker at your convenience.
- */
- openTextMarker(props: MarkerProps): void {
- const { id, hover, className, ...options } = props;
- const startIndex = this.getLastIndex() + this.bufferedText.length;
- this.stacked.push({ startIndex, id, hover, className, options });
- }
-
- /**
- Closes the last opened marker.
- */
- closeTextMarker(): void {
- const tag = this.stacked.pop();
- if (tag) {
- const stopIndex = this.getLastIndex() + this.bufferedText.length;
- this.bufferedTags.push({ stopIndex, ...tag });
- this.armBatch();
- }
- }
-
- /** Lookup for the text markers associated with a marker identifier.
- Remove the marked tags from the buffered tag array. */
- findTextMarker(id: string): TextMarker[] {
- this.doFlushText();
- this.bufferedTags.forEach((tg, idx) => {
- if (tg?.id === id) {
- this.doMark(tg);
- this.bufferedTags[idx] = undefined;
- }
- });
- return this.textmarkers.get(id) ?? [];
- }
-
- /** Lopokup for a hover class. */
- findHover(className: string): CSSMarker | undefined {
- return this.cssmarkers.get(className);
- }
-
- // --------------------------------------------------------------------------
- // --- Highlighter
- // --------------------------------------------------------------------------
-
- /**
- Define highlighter.
-
- @param fn - highlighter, `fn(id)` shall return a className to apply
- on text markers with the provided identifier.
- */
- setDecorator(fn: Decorator): void {
- this.decorator = fn;
- this.emit('decorated');
- }
-
- /**
- Current highlighter.
- */
- getDecorator(): Decorator | undefined { return this.decorator; }
-
- /**
- Rehighlight document.
-
- Emits the `'decorated'` event to make editors
- updating the decorations of identified text markers.
-
- This can be used when decoration shall be re-computed,
- even if the decoration function was not modified.
-
- The method is bound to `this`.
- */
- updateDecorations(): void { this.emit('decorated'); }
-
- // --------------------------------------------------------------------------
- // --- Edited State
- // --------------------------------------------------------------------------
-
- /**
- Set edited state.
-
- The method is automatically invoked by editor views when the user actually
- edit the document. The state is _not_ modified when modifying the document
- from buffer's own methods, _eg._ `append()` and `clear()`.
-
- The method fires the `'edited'` event on modifications. This method is
- bound to `this`, hence `this.setEdited` can be used as a valid callback
- function.
-
- @param state - the new edited state (defaults to `true`).
- */
- setEdited(state = true): void {
- if (state !== this.edited) {
- this.edited = state;
- this.emit('edited', state);
- }
- }
-
- /**
- Set focused state.
-
- The method is automatically invoked by editor views when they gain or lose
- focus or when the user actually interact with the view,
- eg. mouse-scrolling, edition, cursor move, etc. The escape key `ESC`
- explicitly relax the _focused_ state, although the editor view might
- actually keep the _focus_.
-
- When a buffer is _focused_, shrinking and auto-scrolling are temporarily
- deactivated to avoid confusing user's experience.
-
- The method fires `'focused'` events on modifications. This method is bound
- to `this`, hence `this.setEdited` can be used as a valid callback function.
-
- @param focus - the new focused state (defaults to `true`).
- */
- setFocused(state = true): void {
- if (state !== this.focused) {
- this.focused = state;
- this.emit('focused', state);
- this.doShrink();
- }
- }
-
- /** Returns the current _edited_ state. */
- isEdited(): boolean { return this.edited; }
-
- /** Returns the current _focused_ state. */
- isFocused(): boolean { return this.focused; }
-
- // --------------------------------------------------------------------------
- // --- Document Scrolling
- // --------------------------------------------------------------------------
-
- /**
- Set (or unset) the maximum number of lines.
-
- By default, the maximum number of lines is set to `10,000` to avoid
- unwanted memory leaks. Setting `null`, `0` of any negative value cancel the
- management of maximum number of lines.
-
- Although CodeMirror is powerfull enough to manage huge buffers, you should
- turn this limit _off_ with care.
- */
- setMaxlines(maxlines = 10000): void {
- this.maxlines = maxlines > 0 ? 1 + maxlines : 0;
- this.doShrink();
- }
-
- /**
- Requires all connected views to scroll to the
- specified line or identified marker.
-
- @param position -
- defaults to the end of buffer (when not focused).
- */
- scroll(position?: string | number): void {
- if (position === undefined) {
- if (!this.focused) {
- this.doFlushText();
- this.emit('scroll', this.document.lastLine());
- }
- } else if (typeof position === 'number') {
- this.doFlushText();
- this.emit('scroll', position);
- } else if (typeof position === 'string') {
- let line = Infinity;
- this.findTextMarker(position).forEach((tm) => {
- const rg = tm.find();
- if (rg && rg.from) {
- const ln = rg.from.line;
- if (ln < line) line = ln;
- }
- });
- if (line !== Infinity)
- this.emit('scroll', line);
- }
- }
-
- /**
- Requires all connected views to select the specified line and to place it
- at the top of their displays.
-
- @param line - the line number to select
- */
- setCursorOnTop(line: number): void {
- this.forEach((cm) => {
- cm.setCursor(cm.lastLine());
- cm.setCursor(line - 1);
- });
- }
-
- // --------------------------------------------------------------------------
- // --- Document Linking
- // --------------------------------------------------------------------------
-
- private onChange(
- _editor: CodeMirror.Editor,
- change: CodeMirror.EditorChange,
- ): void {
- if (change.origin !== 'buffer') {
- this.setEdited(true);
- this.cacheIndex = -1;
- }
- this.emit('change');
- }
-
- /**
- Binds this buffer to a CodeMirror instance.
-
- Uses CodeMirror linked documents to allow several CodeMirror instances to
- be linked to the same buffer. Can be released with [[unlink]].
-
- @param cm - code mirror instance to link this document in.
- */
- link(cm: CodeMirror.Editor): void {
- const newDoc = this.document.linkedDoc(
- { sharedHist: true, mode: undefined },
- );
- cm.swapDoc(newDoc);
- cm.on('change', this.onChange);
- this.editors.push(cm);
- }
-
- /**
- Release a linked CodeMirror document previously linked with [[link]].
- @param cm - the code mirror instance to unlink
- */
- unlink(cm: CodeMirror.Editor): void {
- const oldDoc = cm.getDoc();
- this.document.unlinkDoc(oldDoc);
- this.editors = this.editors.filter((cm0) => {
- if (cm === cm0) {
- cm.off('change', this.onChange);
- return false;
- }
- return true;
- });
- }
-
- /**
- Iterates over each linked CodeMirror instances
-
- The operation `fn` is performed on each code mirror
- instance currently linked to this buffer.
-
- Exceptions raised by `fn` are catched and dumped in the console.
- */
- forEach(fn: (editor: CodeMirror.Editor) => void): void {
- this.editors.forEach((cm) => {
- try { fn(cm); } catch (e) { D.error(e); }
- });
- }
-
- // --------------------------------------------------------------------------
- // --- Update Operations
- // --------------------------------------------------------------------------
-
- /* Append Operation */
- private doFlushText(): void {
- const text = this.bufferedText;
- if (text.length > 0) {
- this.bufferedText = '';
- const doc = this.document;
- const start = doc.posFromIndex(Infinity);
- doc.replaceRange(text, start, undefined, 'buffer');
- this.cacheIndex = -1;
- this.doShrink();
- }
- }
-
- /* Shrink Operation */
- private doShrink(): void {
- const lines = this.document.lineCount();
- if (lines > this.maxlines) {
- const p = this.document.firstLine();
- const q = p + lines - this.maxlines;
- this.document.replaceRange(
- '',
- { line: p, ch: 0 },
- { line: q, ch: 0 },
- 'buffer',
- );
- this.cacheIndex = -1;
- }
- }
-
- /* Close Operation */
- private doMark(tag: BufferedMarker): void {
- const { id, hover, className, startIndex, stopIndex } = tag;
- let markerId;
- if (id || hover) {
- markerId = `dome-xHover-${this.markid++}`;
- const cmark = {
- id,
- classNameId: markerId,
- hover: hover ?? (id !== undefined),
- length: stopIndex - startIndex,
- };
- this.cssmarkers.set(markerId, cmark);
- }
- const fullClassName = [
- 'dome-xMarked',
- id && (`dome-xMark-${id}`),
- markerId,
- className,
- ].filter((s) => !!s).join(' ');
- const options = {
- shared: true,
- className: fullClassName,
- ...tag.options,
- };
- const doc = this.document;
- const start = doc.posFromIndex(startIndex);
- const stop = doc.posFromIndex(stopIndex);
- const marker = doc.markText(start, stop, options);
- if (id) {
- const markers = this.textmarkers;
- const ms = markers.get(id);
- if (ms === undefined)
- markers.set(id, [marker]);
- else
- ms.push(marker);
- }
- }
-
- private doFilterTags(): BufferedTag[] {
- const tgs = this.bufferedTags;
- if (tgs.length > 0 && this.editors.length > 0) {
- let lmin = Infinity;
- let lmax = 0;
- this.forEach((cm) => {
- const { from: fr, to } = cm.getViewport();
- if (to > lmax) lmax = to;
- if (fr < lmin) lmin = fr;
- });
- if (lmin <= lmax) tgs.sort(byVisibleTag(lmin, lmax + BATCH_MARGINS));
- }
- return tgs.splice(0, BATCH_OPS);
- }
-
- private getLastIndex(): number {
- if (this.cacheIndex < 0) {
- const doc = this.document;
- const line = doc.lastLine() + 1;
- this.cacheIndex = doc.indexFromPos({ line, ch: 0 });
- }
- return this.cacheIndex;
- }
-
- // --------------------------------------------------------------------------
- // --- Batched Operations
- // --------------------------------------------------------------------------
-
- private armBatch(): void {
- if (!this.batched) {
- this.batched = true;
- setTimeout(this.doBatch, BATCH_DELAY);
- }
- }
-
- /* Batch Operation */
- private doBatch(): void {
- this.batched = false;
- if (!this.bufferedText.length && !this.bufferedTags.length) return;
- try {
- // Start Operations
- this.forEach((cm) => cm.startOperation());
- // Flush Text
- this.doFlushText();
- // Mark Tags
- this.doFilterTags().forEach((tg) => { if (tg) this.doMark(tg); });
- // End Operations
- this.forEach((cm) => cm.endOperation());
- } finally {
- if (this.bufferedTags.length > 0)
- this.armBatch();
- }
- }
-
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/text/editors.tsx b/ivette/src/dome/renderer/text/editors.tsx
deleted file mode 100644
index 1153f41e132c577bae2b08ad91144408382cf040..0000000000000000000000000000000000000000
--- a/ivette/src/dome/renderer/text/editors.tsx
+++ /dev/null
@@ -1,566 +0,0 @@
-/* ************************************************************************ */
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2023 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* alternatives) */
-/* */
-/* you can redistribute it and/or modify it under the terms of the GNU */
-/* Lesser General Public License as published by the Free Software */
-/* Foundation, version 2.1. */
-/* */
-/* It is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU Lesser General Public License for more details. */
-/* */
-/* See the GNU Lesser General Public License version 2.1 */
-/* for more details (enclosed in the file licenses/LGPLv2.1). */
-/* */
-/* ************************************************************************ */
-
-// --------------------------------------------------------------------------
-// --- Text Documents
-// --------------------------------------------------------------------------
-
-/**
- @packageDocumentation
- @module dome/text/editors
-*/
-
-import _ from 'lodash';
-import React from 'react';
-import * as Dome from 'dome';
-import * as Themes from 'dome/themes';
-import { Vfill } from 'dome/layout/boxes';
-import CodeMirror, { EditorConfiguration } from 'codemirror/lib/codemirror';
-import { RichTextBuffer, CSSMarker, Decorator } from './buffers';
-
-import './style.css';
-import './dark-code.css';
-import 'codemirror/lib/codemirror.css';
-import 'codemirror/addon/fold/foldcode';
-import 'codemirror/addon/fold/foldgutter';
-import 'codemirror/addon/fold/comment-fold';
-import 'codemirror/addon/fold/foldgutter.css';
-
-const CSS_HOVERED = 'dome-xText-hover';
-const CSS_SELECTED = 'dome-xText-select';
-
-const D = new Dome.Debug('Dome');
-
-/* --------------------------------------------------------------------------*/
-/* --- View Properties --- */
-/* --------------------------------------------------------------------------*/
-
-export interface MarkerCallback {
- (id: string, meta?: boolean): void;
-}
-
-/**
- Text Editor configuration.
-
- Inherits CodeMirror
- [EditorConfiguration](https://codemirror.net/doc/manual.html#config)
- options.
- */
-
-export interface TextProps extends CodeMirror.EditorConfiguration {
-
- /** The buffer to view. */
- buffer: RichTextBuffer | undefined;
-
- /** The currently selected marker identifier. */
- selection?: string;
-
- /** Callback on hovered marker, if some. */
- onHover?: (id?: string) => void;
-
- /** Callback on identified marker selection. */
- onSelection?: MarkerCallback;
-
- /** Callback on identified marker right-click. */
- onContextMenu?: MarkerCallback;
-
- /** Font Size. */
- fontSize?: number;
-
- /** Display or hide the component (true by default). */
- display?: boolean;
-
- /** Additional className for the text container. */
- className?: string;
-
- /** Additional style. */
- style?: React.CSSProperties;
-
-}
-
-/* --------------------------------------------------------------------------*/
-/* --- CodeMirror Configuration Utils ---*/
-/* --------------------------------------------------------------------------*/
-
-function getConfig(props: TextProps): CodeMirror.EditorConfiguration {
- const {
- buffer,
- selection,
- onSelection,
- onContextMenu,
- fontSize,
- ...config
- } = props;
- return config;
-}
-
-type MouseEvt = React.MouseEvent<HTMLDivElement, MouseEvent>;
-type CMoption = keyof EditorConfiguration;
-
-function forEachOption(
- config: EditorConfiguration,
- fn: (opt: CMoption) => void,
-): void {
- (Object.keys(config) as (keyof EditorConfiguration)[]).forEach(fn);
-}
-
-interface _Decoration {
- classNameId: string;
- decoration: string | undefined;
-}
-
-// --------------------------------------------------------------------------
-// --- Code Mirror Instance Wrapper
-// --------------------------------------------------------------------------
-
-class CodeMirrorWrapper extends React.Component<TextProps> {
-
- private currentParent?: Element | null;
- private currentHeight?: number;
- private currentWidth?: number;
- private rootElement: HTMLDivElement | null = null;
- private codeMirror?: CodeMirror.Editor;
- private refreshPolling?: NodeJS.Timeout;
-
- // Currently hovered 'dome-xHover-nnn'
- private marker?: CSSMarker;
-
- // Maps hovered 'dome-xMark-id' to their decorations
- private decorations = new Map<string, string>();
-
- constructor(props: TextProps) {
- super(props);
- this.mountPoint = this.mountPoint.bind(this);
- this.refresh = this.refresh.bind(this);
- this.autoRefresh = this.autoRefresh.bind(this);
- this.onBlur = this.onBlur.bind(this);
- this.onFocus = this.onFocus.bind(this);
- this.onScroll = this.onScroll.bind(this);
- this.onClick = this.onClick.bind(this);
- this.onContextMenu = this.onContextMenu.bind(this);
- this.onMouseMove = this.onMouseMove.bind(this);
- this.handleKey = this.handleKey.bind(this);
- this.handleUpdate = this.handleUpdate.bind(this);
- this.handleHover = _.throttle(this.handleHover, 50);
- this.handleScrollTo = this.handleScrollTo.bind(this);
- }
-
- // --------------------------------------------------------------------------
- // --- Mounting
- // --------------------------------------------------------------------------
-
- mountPoint(elt: HTMLDivElement | null): void {
- this.rootElement = elt;
- if (elt !== null) {
- // Mounting...
- const { buffer } = this.props;
- const config = getConfig(this.props);
- this.codeMirror = CodeMirror(elt, { value: '' });
- if (buffer) {
- buffer.link(this.codeMirror);
- buffer.on('decorated', this.handleUpdate);
- buffer.on('scroll', this.handleScrollTo);
- }
- // Passing all options to constructor does not work (Cf. CodeMirror's BTS)
- forEachOption(
- config, (opt) => this.codeMirror?.setOption(opt, config[opt]),
- );
- // Binding events to view
- this.codeMirror.on('update', this.handleUpdate);
- this.codeMirror.on('keyHandled', this.handleKey);
- Dome.update.on(this.refresh);
- // Auto refresh
- this.refreshPolling = setInterval(this.autoRefresh, 250);
- this.handleUpdate();
- } else {
- // Unmounting...
- if (this.refreshPolling) {
- clearInterval(this.refreshPolling);
- this.refreshPolling = undefined;
- }
- Dome.update.off(this.refresh);
- const { buffer } = this.props;
- if (this.codeMirror && buffer) {
- buffer.unlink(this.codeMirror);
- buffer.off('decorated', this.handleUpdate);
- buffer.off('scroll', this.handleScrollTo);
- }
- this.codeMirror = undefined;
- this.marker = undefined;
- this.decorations.clear();
- }
- }
-
- // --------------------------------------------------------------------------
- // --- Auto Refresh
- // --------------------------------------------------------------------------
-
- refresh(): void {
- const elt = this.rootElement;
- const cm = this.codeMirror;
- if (cm && elt) {
- this.currentWidth = elt.offsetWidth;
- this.currentHeight = elt.offsetHeight;
- this.currentParent = elt.offsetParent;
- cm.refresh();
- }
- }
-
- // Polled every 250ms
- autoRefresh(): void {
- const elt = this.rootElement;
- const cm = this.codeMirror;
- if (cm && elt) {
- const eltW = elt.offsetWidth;
- const eltH = elt.offsetHeight;
- const eltP = elt.offsetParent;
- if (eltW !== this.currentWidth ||
- eltH !== this.currentHeight ||
- eltP !== this.currentParent) {
- this.currentWidth = eltW;
- this.currentHeight = eltH;
- this.currentParent = eltP;
- cm.refresh();
- }
- }
- }
-
- // --------------------------------------------------------------------------
- // --- Hover
- // --------------------------------------------------------------------------
-
- _findMarker(elt: Element): CSSMarker | undefined {
- const { buffer } = this.props;
- if (buffer) {
- let best: CSSMarker | undefined;
- elt.classList.forEach((name) => {
- const marker = buffer.findHover(name);
- if (marker && (!best || marker.length < best.length)) best = marker;
- });
- return best;
- }
- return undefined;
- }
-
- // eslint-disable-next-line class-methods-use-this
- _findDecoration(
- classes: DOMTokenList,
- buffer: RichTextBuffer,
- decorator: Decorator,
- ): _Decoration | undefined {
- let bestMarker: CSSMarker | undefined;
- let bestDecorated: CSSMarker | undefined;
- let bestDecoration: string | undefined;
- classes.forEach((name) => {
-
- const marker = buffer.findHover(name);
- const id = marker && marker.id;
- const decoration = id && decorator(id);
-
- if (marker && (!bestMarker || marker.length < bestMarker.length)) {
- bestMarker = marker;
- }
-
- if (marker && decoration &&
- (!bestDecorated || marker.length < bestDecorated.length)) {
- bestDecorated = marker;
- bestDecoration = decoration;
- }
-
- });
- return bestMarker ? {
- classNameId: bestMarker.classNameId,
- decoration: bestDecoration,
- } : undefined;
- }
-
- _markElementsWith(classNameId: string, className: string): void {
- const root = this.rootElement;
- const toMark = root && root.getElementsByClassName(classNameId);
- if (toMark) {
- const n = toMark.length;
- if (n === 0) return;
- for (let k = 0; k < n; k++) toMark[k].classList.add(className);
- }
- }
-
- _unmarkElementsWith(className: string): void {
- const root = this.rootElement;
- const toUnmark = root && root.getElementsByClassName(className);
- if (toUnmark) {
- const n = toUnmark.length;
- if (n === 0) return;
- const elts: Element[] = new Array(n);
- for (let k = 0; k < n; k++) elts[k] = toUnmark[k];
- elts.forEach((elt) => elt.classList.remove(className));
- }
- }
-
- handleHover(target: Element): void {
- // Throttled (see constructor)
- const oldMarker = this.marker;
- const newMarker = this._findMarker(target);
- if (oldMarker !== newMarker) {
- if (oldMarker) this._unmarkElementsWith(CSS_HOVERED);
- if (newMarker && newMarker.hover)
- this._markElementsWith(newMarker.classNameId, CSS_HOVERED);
- this.marker = newMarker;
- const callback = this.props.onHover;
- if (callback) callback(newMarker?.id);
- }
- }
-
- handleUpdate(): void {
- const root = this.rootElement;
- const marked = root && root.getElementsByClassName('dome-xMarked');
- if (!marked) return;
- const n = marked.length;
- if (n === 0) return;
- const { marker } = this;
- const hovered = (marker && marker.hover) ? marker.classNameId : undefined;
- const { selection } = this.props;
- const selected = selection && (`dome-xMark-${selection}`);
- const { buffer } = this.props;
- const decorator = buffer?.getDecorator();
- if (!hovered && !selection && !decorator) return;
- const newDecorations = new Map<string, string>();
- for (let k = 0; k < n; k++) {
- const elt = marked[k];
- const classes = elt.classList;
- if (hovered && classes.contains(hovered)) classes.add(CSS_HOVERED);
- if (selected && classes.contains(selected)) classes.add(CSS_SELECTED);
- if (buffer && decorator) {
- const deco = this._findDecoration(classes, buffer, decorator);
- if (deco) {
- const prev = this.decorations.get(deco.classNameId);
- const curr = deco.decoration;
- if (prev && prev !== curr) classes.remove(prev);
- if (curr) {
- classes.add(curr);
- newDecorations.set(deco.classNameId, curr);
- }
- }
- }
- }
- this.decorations = newDecorations;
- }
-
- onMouseMove(evt: MouseEvt): void {
- // Not throttled (can not leak Synthetic Events)
- const tgt = evt.target;
- if (tgt instanceof Element) this.handleHover(tgt);
- }
-
- onMouseClick(evt: MouseEvt, callback: MarkerCallback | undefined): void {
- // No need for throttling
- if (callback) {
- const { target } = evt;
- if (target instanceof Element) {
- const marker = this._findMarker(target);
- if (marker && marker.id) callback(marker.id, evt.altKey);
- }
- }
- this.props.buffer?.setFocused(true);
- }
-
- onClick(evt: MouseEvt): void {
- this.onMouseClick(evt, this.props.onSelection);
- }
-
- onContextMenu(evt: MouseEvt): void {
- this.onMouseClick(evt, this.props.onContextMenu);
- }
-
- // --------------------------------------------------------------------------
- // --- Scrolling
- // --------------------------------------------------------------------------
-
- handleScrollTo(line: number): void {
- try {
- const cm = this.codeMirror;
- return cm && cm.scrollIntoView({ line, ch: 0 });
- } catch (_error) {
- D.warn(`unable to scroll to line ${line}: out of range.`);
- }
- }
-
- // --------------------------------------------------------------------------
- // --- Focus
- // --------------------------------------------------------------------------
-
- handleKey(_cm: CodeMirror.Editor, key: string, _evt: Event): void {
- switch (key) {
- case 'Esc':
- this.props.buffer?.setFocused(false);
- break;
- default:
- this.props.buffer?.setFocused(true);
- break;
- }
- }
-
- onFocus(): void { this.props.buffer?.setFocused(true); }
- onBlur(): void { this.props.buffer?.setFocused(false); }
- onScroll(): void {
- const cm = this.codeMirror;
- const { buffer } = this.props;
- if (cm && buffer) {
- const rect = cm.getScrollInfo();
- const delta = rect.height - rect.top - rect.clientHeight;
- buffer.setFocused(delta > 0);
- }
- }
-
- // --------------------------------------------------------------------------
- // --- Rendering
- // --------------------------------------------------------------------------
-
- shouldComponentUpdate(newProps: TextProps): boolean {
- const cm = this.codeMirror;
- if (cm) {
- // Swap documents if necessary
- const {
- buffer: oldBuffer,
- selection: oldSelect,
- fontSize: oldFont,
- } = this.props;
- const {
- buffer: newBuffer,
- selection: newSelect,
- fontSize: newFont,
- } = newProps;
- if (oldBuffer !== newBuffer) {
- if (oldBuffer) oldBuffer.unlink(cm);
- if (newBuffer) newBuffer.link(cm);
- else cm.setValue('');
- }
- const oldConfig = getConfig(this.props);
- const newConfig = getConfig(newProps);
- // Incremental update options
- forEachOption(oldConfig, (opt) => {
- if (!(opt in newConfig)) {
- const defValue = CodeMirror.defaults[opt];
- if (defValue)
- cm.setOption(opt, defValue);
- }
- });
- forEachOption(newConfig, (opt) => {
- const oldValue = oldConfig[opt];
- const newValue = newConfig[opt];
- if (newValue !== oldValue) {
- cm.setOption(opt, newValue);
- }
- });
- // Update selection
- if (oldSelect !== newSelect) {
- const selected = `dome-xMark-${newSelect}`;
- if (oldSelect) this._unmarkElementsWith(CSS_SELECTED);
- if (newSelect) this._markElementsWith(selected, CSS_SELECTED);
- }
- // Refresh on new font
- if (oldFont !== newFont) setImmediate(this.refresh);
- }
- // Keep mounted node unchanged
- return false;
- }
-
- render(): JSX.Element {
- return (
- <div
- className="dome-xText"
- ref={this.mountPoint}
- onClick={this.onClick}
- onContextMenu={this.onContextMenu}
- onBlur={this.onBlur}
- onFocus={this.onFocus}
- onScroll={this.onScroll}
- onMouseMove={this.onMouseMove}
- onMouseLeave={this.onMouseMove}
- />
- );
- }
-
-}
-
-// --------------------------------------------------------------------------
-// --- Text View
-// --------------------------------------------------------------------------
-
-/** #### Text Editor.
-
- A component rendering the content of a text buffer, that shall be instances
- of the `Buffer` base class.
-
- The view is based on a [CodeMirror](https://codemirror.net) component linked
- with the internal Code Mirror Document from the associated buffer.
-
- Multiple views might share the same buffer as source content. The buffer will
- be kept in sync with all its linked views.
-
- The Text component never update its mounted NODE element, however, all
- property modifications (including buffer) are propagated to the internal
- CodeMirror instance. Undefined properties are set (or reset) to the
- CodeMirror defaults.
-
- #### Themes
-
- The CodeMirror `theme` option allow you to style your document, especially
- when using modes.
-
- By default, CodeMirror uses the `'default'` theme in _light_ theme and the
- `'dark-code'` theme in _dark_ theme. The `'dark-code'` is provided by Dome,
- Cf. `./dark-mode.css` in the source distribution.
-
- To use other custom themes, you shall load the associated CSS style
- sheet. For instance, to use the `'ambiance'` theme provided with CodeMirror,
- you shall import `'codemirror/theme/ambiance.css'` somewhere in your
- application.
-
- #### Modes & Adds-On
-
- You can install modes and adds-on provided by the CodeMirror distribution by
- simply importing (once, before being used) the associated modules in your
- application. For instance, to use the `'javascript'` mode option, you shall
- import `'codemirror/mode/javascript/javascript.js'` file in your application.
-
- #### Further Customization
-
- You can register your own extensions directly into the global `CodeMirror`
- class instance. However, the correct instance must be retrieved by using
- `import CodeMirror from 'codemirror/lib/codemirror.js'` ; using `from
- 'codemirror'` returns a different instance of `CodeMirror` class and will not
- work. */
-export function Text(props: TextProps): JSX.Element {
- const [appTheme] = Themes.useColorTheme();
- let { className, style, fontSize, theme: usrTheme, ...cmprops } = props;
- if (fontSize !== undefined && fontSize < 4) fontSize = 4;
- if (fontSize !== undefined && fontSize > 48) fontSize = 48;
- const theme = usrTheme ?? (appTheme === 'dark' ? 'dark-code' : 'default');
- const display = props.display === false ? 'none' : undefined;
- return (
- <Vfill className={className} style={{ ...style, fontSize, display }}>
- <CodeMirrorWrapper fontSize={fontSize} theme={theme} {...cmprops} />
- </Vfill>
- );
-}
-
-// --------------------------------------------------------------------------
diff --git a/ivette/src/dome/renderer/text/richtext.tsx b/ivette/src/dome/renderer/text/richtext.tsx
index 22405ddb87ce1895164dd4205cf0ce941d0c81ed..936ea7ad45aa74d0f47b305d1116e54525bdbaa1 100644
--- a/ivette/src/dome/renderer/text/richtext.tsx
+++ b/ivette/src/dome/renderer/text/richtext.tsx
@@ -258,13 +258,16 @@ export class TextBuffer extends TextProxy {
return this.contents ?? this.text.toString();
}
- append(data: string): void {
- const view = this.proxy;
- if (view) { appendContents(view, data); }
- else {
- this.text = this.toText().append(textOf(data));
- this.contents = undefined;
- // invariant established
+ append(...values: unknown[]): void {
+ if (values.length > 0) {
+ const data = values.join(' ');
+ const view = this.proxy;
+ if (view) { appendContents(view, data); }
+ else {
+ this.text = this.toText().append(textOf(data));
+ this.contents = undefined;
+ // invariant established
+ }
}
}
diff --git a/ivette/src/dome/renderer/text/style.css b/ivette/src/dome/renderer/text/style.css
index a572476d794c4e688d62f2247b591b733df7b879..ca2d76573124a34c36003b3d50f84b96cb6685ab 100644
--- a/ivette/src/dome/renderer/text/style.css
+++ b/ivette/src/dome/renderer/text/style.css
@@ -1,33 +1,3 @@
-/* -------------------------------------------------------------------------- */
-/* --- Styling Code Editors --- */
-/* -------------------------------------------------------------------------- */
-
-.dome-xText {
- flex: 1 1 auto ;
- overflow: hidden ;
- position: relative ;
- fontSize: smaller ;
-}
-
-.dome-xText .CodeMirror {
- width: 100% ;
- height: 100% ;
- line-height: 1.2 !important;
- text-shadow: none !important;
-}
-
-.dome-xText-hover {
- background: var(--code-hover) ;
-}
-
-.dome-xText-select {
- background: var(--code-select) !important ;
-}
-
-.dome-xText-select.dome-xText-hover {
- background: var(--code-select-hover) !important ;
-}
-
/* -------------------------------------------------------------------------- */
/* --- Styling Page --- */
/* -------------------------------------------------------------------------- */
@@ -240,6 +210,7 @@
.cm-number { color: var(--codemirror-number); }
.cm-keyword { color: var(--codemirror-keyword); }
+.cm-activeLine
.cm-active-line { background-color: var(--background); }
/* -------------------------------------------------------------------------- */
diff --git a/ivette/src/dome/template/makefile.packages b/ivette/src/dome/template/makefile.packages
index 3d689992f112c66ac9567c506f195c0a35bced37..f42f27f0b7d0f1cb82d2582c85beff9b8fa26413 100644
--- a/ivette/src/dome/template/makefile.packages
+++ b/ivette/src/dome/template/makefile.packages
@@ -50,7 +50,6 @@ DOME_APP_PACKAGES= \
react-virtualized \
react-draggable \
react-fast-compare \
- codemirror@^5 \
diff
# --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx
index ed9fbb8d232986f67d1d9dc8e05cd6928ea93862..aa96434523bfcc635fe253f699de218802b3ec58 100644
--- a/ivette/src/frama-c/richtext.tsx
+++ b/ivette/src/frama-c/richtext.tsx
@@ -31,46 +31,11 @@
import React from 'react';
import * as Dome from 'dome';
-import * as DomeBuffers from 'dome/text/buffers';
import * as KernelData from 'frama-c/kernel/api/data';
import { classes } from 'dome/misc/utils';
const D = new Dome.Debug('Utils');
-// --------------------------------------------------------------------------
-// --- Print Utilities
-// --------------------------------------------------------------------------
-
-/**
- * Print text containing tags into buffer.
- * @param buffer Rich text buffer to print into.
- * @param text Actual text containing tags.
- * @param options Specify particular marker options.
- */
-export function printTextWithTags(
- buffer: DomeBuffers.RichTextBuffer,
- text: KernelData.text,
- options?: DomeBuffers.MarkerProps,
-): void {
- if (Array.isArray(text)) {
- const tag = text[0];
- const marker = typeof (tag) === 'string';
- if (marker) {
- buffer.openTextMarker({ id: tag, ...options ?? {} });
- }
- for (let k = marker ? 1 : 0; k < text.length; k++) {
- printTextWithTags(buffer, text[k], options);
- }
- if (marker) {
- buffer.closeTextMarker();
- }
- } else if (typeof text === 'string') {
- buffer.append(text);
- } else {
- D.error('Unexpected text', text);
- }
-}
-
// --------------------------------------------------------------------------
// --- Lightweight Text Renderer
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/server.ts b/ivette/src/frama-c/server.ts
index defba404bcb97d36f12777202b4734a5bfbc6cde..7cab67fc55c2bd54b0e90048cff22c119f926f91 100644
--- a/ivette/src/frama-c/server.ts
+++ b/ivette/src/frama-c/server.ts
@@ -36,7 +36,7 @@ import React from 'react';
import * as Dome from 'dome';
import * as System from 'dome/system';
import * as Json from 'dome/data/json';
-import { RichTextBuffer } from 'dome/text/buffers';
+import { TextBuffer } from 'dome/text/richtext';
import { ChildProcess } from 'child_process';
import { client } from './client_socket';
// import { client } from './client_zmq';
@@ -136,7 +136,7 @@ let killingTimer: NodeJS.Timeout | undefined;
// --------------------------------------------------------------------------
/** The server console buffer. */
-export const buffer = new RichTextBuffer();
+export const buffer = new TextBuffer();
// --------------------------------------------------------------------------
// --- Server Status
@@ -231,7 +231,7 @@ export async function start(): Promise<void> {
try {
await _launch();
} catch (error) {
- buffer.log('[frama-c]', error);
+ buffer.append('[frama-c]', error, '\n');
_exit(false);
}
return;
@@ -480,27 +480,21 @@ async function _launch(): Promise<void> {
sockaddr && System.remove(sockaddr);
});
process = await System.spawn(command, params, options);
- const logger = (text: string | string[]): void => {
- buffer.append(text);
- if (text.indexOf('\n') >= 0) {
- buffer.scroll();
- }
- };
- process?.stdout?.on('data', logger);
- process?.stderr?.on('data', logger);
+ process?.stdout?.on('data', buffer.append);
+ process?.stderr?.on('data', buffer.append);
process?.on('exit', (code: number | null, signal: string | null) => {
if (signal !== null) {
- buffer.log('[frama-c]', signal);
+ buffer.append('[frama-c]', signal, '\n');
_exit(false);
return;
}
if (code !== 0) {
- buffer.log('[frama-c] exit', code);
+ buffer.append('[frama-c] exit', code, '\n');
_exit(true);
return;
}
if (Dome.DEVEL)
- buffer.log('[frama-c] terminated.');
+ buffer.append('[frama-c] terminated.\n');
_exit(false);
return;
});
diff --git a/ivette/src/ivette/prefs.tsx b/ivette/src/ivette/prefs.tsx
index 61a7835539e8299f54ac3fa391212d2a1f83b009..4bb16c1276941ae45edf8abe956b20899de332d4 100644
--- a/ivette/src/ivette/prefs.tsx
+++ b/ivette/src/ivette/prefs.tsx
@@ -34,7 +34,6 @@ import * as Dome from 'dome';
import * as Themes from 'dome/themes';
import * as Toolbar from 'dome/frame/toolbars';
import * as Settings from 'dome/data/settings';
-import 'codemirror/mode/clike/clike';
/* -------------------------------------------------------------------------- */
/* --- Theme Switcher Button --- */
diff --git a/ivette/src/renderer/Controller.tsx b/ivette/src/renderer/Controller.tsx
index d69dd2269894463c2bd0bab86a1673ba1c7f4db5..cf837e3febd75abf8bf6c60c31cf1cd6abf4c86b 100644
--- a/ivette/src/renderer/Controller.tsx
+++ b/ivette/src/renderer/Controller.tsx
@@ -33,8 +33,7 @@ import * as Toolbars from 'dome/frame/toolbars';
import { IconButton } from 'dome/controls/buttons';
import { LED, LEDstatus } from 'dome/controls/displays';
import { Label, Code } from 'dome/controls/labels';
-import { RichTextBuffer } from 'dome/text/buffers';
-import { Text } from 'dome/text/editors';
+import { TextBuffer, TextView } from 'dome/text/richtext';
import { resolve } from 'dome/system';
import * as Ivette from 'ivette';
@@ -223,36 +222,40 @@ export const Control = (): JSX.Element => {
// --- Server Console
// --------------------------------------------------------------------------
-const editor = new RichTextBuffer();
+const editor = new TextBuffer();
const RenderConsole = (): JSX.Element => {
const scratch = React.useRef([] as string[]);
const [cursor, setCursor] = React.useState(-1);
const [isEmpty, setEmpty] = React.useState(true);
- const [noTrash, setNoTrash] = React.useState(true);
+ const [noTrash, _setNoTrash] = React.useState(true);
const [history, setHistory] = useHistory();
+ /*
React.useEffect(() => {
const callback = (): void => {
- const cmd = editor.getValue().trim();
+ const cmd = editor.toString().trim();
setEmpty(cmd === '');
setNoTrash(noTrash && cmd === history[0]);
};
editor.on('change', callback);
return () => { editor.off('change', callback); };
});
+ */
- const [maxLines] = Settings.useGlobalSettings(Preferences.ConsoleScrollback);
+ const [_maxLines] = Settings.useGlobalSettings(Preferences.ConsoleScrollback);
+ /*
React.useEffect(() => {
Server.buffer.setMaxlines(maxLines);
});
+ */
const doReload = (): void => {
const cfg = Server.getConfig();
const hst = insertConfig(history, cfg);
const cmd = hst[0];
scratch.current = hst.slice();
- editor.setValue(cmd);
+ editor.setContents(cmd);
setEmpty(cmd === '');
setHistory(hst);
setCursor(0);
@@ -268,7 +271,7 @@ const RenderConsole = (): JSX.Element => {
};
const doExec = (): void => {
- const cfg = buildServerCommand(editor.getValue());
+ const cfg = buildServerCommand(editor.toString());
const hst = insertConfig(history, cfg);
setHistory(hst);
setCursor(-1);
@@ -280,11 +283,11 @@ const RenderConsole = (): JSX.Element => {
const doMove = (target: number): (undefined | (() => void)) => {
if (0 <= target && target < history.length && target !== cursor)
return (): void => {
- const cmd = editor.getValue();
+ const cmd = editor.toString();
const pad = scratch.current;
pad[cursor] = cmd;
const cmd2 = pad[target];
- editor.setValue(cmd2);
+ editor.setContents(cmd2);
setEmpty(cmd2 === '');
setCursor(target);
};
@@ -301,7 +304,7 @@ const RenderConsole = (): JSX.Element => {
pad.splice(cursor, 1);
setHistory(hst);
const next = cursor > 0 ? cursor - 1 : 0;
- editor.setValue(pad[next]);
+ editor.setContents(pad[next]);
setCursor(next);
}
};
@@ -363,9 +366,8 @@ const RenderConsole = (): JSX.Element => {
title="Toggle command line editing"
/>
</Ivette.TitleBar>
- <Text
- buffer={edited ? editor : Server.buffer}
- mode="text"
+ <TextView
+ text={edited ? editor : Server.buffer}
readOnly={!edited}
/>
</>
diff --git a/ivette/yarn.lock b/ivette/yarn.lock
index f1883e3f52622fdf7dee22f007ef7ead226b8a6b..398f58fd1f382be0632dc429fdaf8ca878622e40 100644
--- a/ivette/yarn.lock
+++ b/ivette/yarn.lock
@@ -3568,11 +3568,6 @@ clsx@^1.0.4, clsx@^1.1.1:
resolved "https://registry.yarnpkg.com/clsx/-/clsx-1.1.1.tgz#98b3134f9abbdf23b2663491ace13c5c03a73188"
integrity sha512-6/bPho624p3S2pMyvP5kKBPXnI3ufHLObBFCfgx+LkeR5lg2XYy2hqZqUf45ypD8COn2bhgGJSUE+l5dhNBieA==
-codemirror@^5:
- version "5.65.15"
- resolved "https://registry.yarnpkg.com/codemirror/-/codemirror-5.65.15.tgz#66899278f44a7acde0eb641388cd563fe6dfbe19"
- integrity sha512-YC4EHbbwQeubZzxLl5G4nlbLc1T21QTrKGaOal/Pkm9dVDMZXMH7+ieSPEOZCtO9I68i8/oteJKOxzHC2zR+0g==
-
collection-visit@^1.0.0:
version "1.0.0"
resolved "https://registry.yarnpkg.com/collection-visit/-/collection-visit-1.0.0.tgz#4bc0373c164bc3291b4d368c829cf1a80a59dca0"
@@ -4250,7 +4245,7 @@ detect-node@^2.0.4:
resolved "https://registry.yarnpkg.com/detect-node/-/detect-node-2.1.0.tgz#c9c70775a49c3d03bc2c06d9a73be550f978f8b1"
integrity sha512-T0NIuQpnTvFDATNuHN5roPwSBG83rFsuO+MXXH9/3N1eFbn4wcPjttvjMLEPWJ0RGUYgQE7cGgS3tNxbqCGM7g==
-diff@:
+diff@^5.1.0:
version "5.1.0"
resolved "https://registry.yarnpkg.com/diff/-/diff-5.1.0.tgz#bc52d298c5ea8df9194800224445ed43ffc87e40"
integrity sha512-D+mk+qE8VC/PAUrlAU34N+VfXev0ghe5ywmpqrawphmVZc1bEfn56uo9qpyGp1p4xpzOHkSW4ztBd6L7Xx4ACw==