From aaaa1a476a96b53137f6d7a18bcbcb4ba566b301 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 5 Dec 2023 15:11:11 +0100
Subject: [PATCH] [ivette/wp] smouth updating & selected part gutters
---
ivette/src/dome/renderer/text/richtext.tsx | 18 ++-----
ivette/src/frama-c/plugins/wp/style.css | 8 ++++
ivette/src/frama-c/plugins/wp/tip.tsx | 56 ++++++++++++++--------
3 files changed, 47 insertions(+), 35 deletions(-)
diff --git a/ivette/src/dome/renderer/text/richtext.tsx b/ivette/src/dome/renderer/text/richtext.tsx
index c6d0293ffc2..03859f53447 100644
--- a/ivette/src/dome/renderer/text/richtext.tsx
+++ b/ivette/src/dome/renderer/text/richtext.tsx
@@ -114,7 +114,8 @@ class DiffBuffer {
function updateContents(view: CM.EditorView, newText: string): void {
const buffer = new DiffBuffer();
diffLines(view.state.doc.toString(), newText).forEach(buffer.add);
- view.dispatch({ changes: buffer.flush() });
+ const changes = buffer.flush();
+ view.dispatch({ changes });
}
/* -------------------------------------------------------------------------- */
@@ -814,19 +815,6 @@ interface Decorator {
gutters : CS.RangeSet<CM.GutterMarker>;
}
-function compareDecorations(a : Decorations, b : Decorations): boolean
-{
- if (a === b) return true;
- if (!a || isDecoration(a)) return false;
- if (!b || isDecoration(b)) return false;
- const n = a.length;
- if (n !== b.length) return false;
- for (let k = 0; k < n; k++)
- if (!compareDecorations(a[k], b[k]))
- return false;
- return true;
-}
-
const DecoratorSpec = CS.Annotation.define<Decorations>();
const DecoratorState = CS.StateField.define<Decorator>({
@@ -839,7 +827,7 @@ const DecoratorState = CS.StateField.define<Decorator>({
update(value: Decorator, tr: CS.Transaction) {
const newSpec : Decorations = tr.annotation(DecoratorSpec) ?? null;
- if (newSpec !== null && !compareDecorations(newSpec, value.spec)) {
+ if (newSpec !== null) {
const builder = new DecorationsBuilder(tr.newDoc);
builder.addSpec(newSpec);
return {
diff --git a/ivette/src/frama-c/plugins/wp/style.css b/ivette/src/frama-c/plugins/wp/style.css
index d396e4c9c4a..eab44e5565f 100644
--- a/ivette/src/frama-c/plugins/wp/style.css
+++ b/ivette/src/frama-c/plugins/wp/style.css
@@ -2,6 +2,14 @@
/* --- WP Panel Styles --- */
/* -------------------------------------------------------------------------- */
+.wp .cm-gutter {
+ width: 3px;
+}
+
+.wp-gutter-part {
+ background: red;
+}
+
.wp.cm-hovered-code,
.wp.cm-hovered-code > span
{
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index dc4e100710b..586ea2c5f98 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -28,8 +28,8 @@ import { Cell } from 'dome/controls/labels';
import { ToolBar, Select, Filler } from 'dome/frame/toolbars';
import { Vfill } from 'dome/layout/boxes';
import {
- MarkDecoration, Decorations,
- Position, TextView
+ MarkDecoration, GutterDecoration, Decorations,
+ Position, Range, TextProxy, TextView,
} from 'dome/text/richtext';
import * as Server from 'frama-c/server';
@@ -116,6 +116,7 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
type Node = TIP.node | undefined;
type Location = { part?: RichText.Tag, term?: RichText.Tag };
+type Target = { selection?: Range, gutters: GutterDecoration[] };
class Sequent {
private readonly contents: string;
@@ -185,6 +186,20 @@ class Sequent {
return ptags[0];
}
+ target(proxy: TextProxy, part?: TIP.part, term?: TIP.term): Target {
+ const tag = this.select(part, term);
+ const gutters: GutterDecoration[] = [];
+ if (tag) {
+ const selection: Range = { offset: tag.offset, length: 0 };
+ const lineFrom = proxy.lineAt(tag.offset+1);
+ const lineTo = proxy.lineAt(tag.endOffset);
+ for (let line = lineFrom; line <= lineTo; line++)
+ gutters.push({ className: 'wp-gutter-part', gutter: '|', line });
+ return { selection, gutters };
+ } else
+ return { selection: undefined, gutters };
+ }
+
locate(position: number): Location {
const isPart = ({ tag }: RichText.Tag): boolean => {
return tag === '#goal' || tag.startsWith('#s');
@@ -227,16 +242,18 @@ function GoalView(props: GoalViewProps): JSX.Element {
const unmangled = focus === 'MEMORY' || focus === 'RAW';
const jtext = States.useRequest(TIP.printSequent, {
node, iformat, rformat, autofocus, unmangled,
+ }, {
+ pending: null,
+ offline: undefined,
+ onError: '',
}) ?? null;
const { part, term } = States.useRequest(TIP.getSelection, node) ?? {};
+ const proxy = React.useMemo(() => new TextProxy(), []);
const sequent = React.useMemo(() => new Sequent(jtext), [jtext]);
- const selection = React.useMemo(
- () => {
- const tag = sequent.select(part, term);
- const selection = tag && { offset: tag.offset, length: 0 };
- return selection;
- },
- [sequent, part, term]
+ React.useEffect(() => proxy.updateContents(sequent.text), [proxy, sequent]);
+ const { selection, gutters } = React.useMemo(
+ () => sequent.target(proxy, part, term),
+ [sequent, proxy, part, term]
);
const [hover, setHover] = React.useState<Decorations>(null);
const onHover = React.useCallback((pos: Position | null) => {
@@ -244,15 +261,13 @@ function GoalView(props: GoalViewProps): JSX.Element {
}, [sequent]);
const onClick = React.useCallback((pos: Position | null) => {
setHover(null);
- if (node) {
- if (pos) {
- const loc = sequent.locate(pos.offset);
- const part = jOption(TIP.jPart)(loc.part?.tag);
- const term = jOption(TIP.jTerm)(loc.term?.tag);
- if (part || term) {
- Server.send(TIP.setSelection, { node, part, term });
- return;
- }
+ if (node && pos) {
+ const loc = sequent.locate(pos.offset);
+ const part = jOption(TIP.jPart)(loc.part?.tag);
+ const term = jOption(TIP.jTerm)(loc.term?.tag);
+ if (part || term) {
+ Server.send(TIP.setSelection, { node, part, term });
+ return;
}
}
Server.send(TIP.clearSelection, node);
@@ -260,9 +275,10 @@ function GoalView(props: GoalViewProps): JSX.Element {
return (
<TextView
readOnly
- text={sequent.text}
+ className='wp'
+ text={proxy}
selection={selection}
- decorations={[hover, sequent.decorations]}
+ decorations={[hover, sequent.decorations, gutters]}
onHover={onHover}
onClick={onClick}
/>
--
GitLab