diff --git a/ivette/src/frama-c/plugins/wp/api/tip/index.ts b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
index 6efc2cf639af0dc686f6fd086c294886b314c321..f1c3ac6961a529da08f2a64c9a231de1b44b2590 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -307,4 +307,23 @@ export const setSelection: Server.SetRequest<
null
>= setSelection_internal;
+const getSelection_internal: Server.GetRequest<
+ node,
+ { part?: part, term?: term }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.wp.tip.getSelection',
+ input: jNode,
+ output: Json.jObject({
+ part: Json.jOption(jPart),
+ term: Json.jOption(jTerm),
+ }),
+ signals: [ { name: 'plugins.wp.tip.printStatus' } ],
+};
+/** Get current selection in proof node */
+export const getSelection: Server.GetRequest<
+ node,
+ { part?: part, term?: term }
+ >= getSelection_internal;
+
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/style.css b/ivette/src/frama-c/plugins/wp/style.css
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..d396e4c9c4a9affa4eed1bc221ebffa852e509ca 100644
--- a/ivette/src/frama-c/plugins/wp/style.css
+++ b/ivette/src/frama-c/plugins/wp/style.css
@@ -0,0 +1,9 @@
+/* -------------------------------------------------------------------------- */
+/* --- WP Panel Styles --- */
+/* -------------------------------------------------------------------------- */
+
+.wp.cm-hovered-code,
+.wp.cm-hovered-code > span
+{
+ background: var(--code-hover);
+}
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 53bf3e0d36e56175d970ce46f1a21e39714bbff6..dc4e100710bc9a63b5fbfd756adec83dcbe74b6f 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -23,7 +23,7 @@
import React from 'react';
import * as Dome from 'dome';
-import type { json } from 'dome/data/json';
+import { jOption, json } from 'dome/data/json';
import { Cell } from 'dome/controls/labels';
import { ToolBar, Select, Filler } from 'dome/frame/toolbars';
import { Vfill } from 'dome/layout/boxes';
@@ -32,6 +32,7 @@ import {
Position, TextView
} from 'dome/text/richtext';
+import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as RichText from 'frama-c/richtext';
import type { text } from 'frama-c/kernel/api/data';
@@ -114,12 +115,13 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
/* -------------------------------------------------------------------------- */
type Node = TIP.node | undefined;
-type Location = { step?: RichText.Tag, term?: RichText.Tag };
+type Location = { part?: RichText.Tag, term?: RichText.Tag };
class Sequent {
private readonly contents: string;
private readonly tags: RichText.Tags;
private readonly style: MarkDecoration[];
+ private readonly index: RichText.TagIndex;
constructor(jtext: text) {
this.contents = RichText.textToString(jtext);
@@ -147,7 +149,7 @@ class Sequent {
addStyle(t, 'cm-type');
return false;
case 'wp:focus':
- addStyle(t, 'cm-hovered-code');
+ addStyle(t, 'cm-multiple-code');
return false;
case 'wp:target':
addStyle(t, 'cm-selected-code');
@@ -155,8 +157,9 @@ class Sequent {
}
return t.tag.startsWith('#');
};
- const { tags } = RichText.textToTags(jtext, filter);
+ const { index, tags } = RichText.textToTags(jtext, filter);
this.tags = tags;
+ this.index = index;
}
get text(): string {
@@ -167,14 +170,42 @@ class Sequent {
return this.style;
}
+ find(tg: string | undefined) : RichText.Tags {
+ return tg ? this.index.get(tg) ?? [] : [];
+ }
+
+ select(part?: TIP.part, term?: TIP.term): RichText.Tag | undefined {
+ const ptags = this.find(part);
+ if (!ptags) return;
+ const etags = this.find(term);
+ if (etags) {
+ const tg = etags.find(e => ptags.find(p => RichText.contains(p, e)));
+ if (tg) return tg;
+ }
+ return ptags[0];
+ }
+
locate(position: number): Location {
- const stepOnly = ({ tag }: RichText.Tag): boolean => {
+ const isPart = ({ tag }: RichText.Tag): boolean => {
return tag === '#goal' || tag.startsWith('#s');
};
- const step = RichText.findTag(this.tags, position, stepOnly);
- if (!step) return {};
- const term = RichText.findTag(step.children, position);
- return { step, term };
+ const part = RichText.findTag(this.tags, position, isPart);
+ if (!part) return {};
+ const term = RichText.findTag(part.children, position);
+ return { part, term };
+ }
+
+ hover(pos: Position | null): Decorations {
+ if (pos) {
+ const { part, term } = this.locate(pos.offset);
+ const range = term ?? part;
+ if (range) {
+ const { offset, endOffset } = range;
+ const length = endOffset - offset;
+ return { className: 'wp cm-hovered-code', offset, length };
+ }
+ }
+ return null;
}
}
@@ -195,33 +226,45 @@ function GoalView(props: GoalViewProps): JSX.Element {
const autofocus = focus === 'AUTOFOCUS' || focus === 'MEMORY';
const unmangled = focus === 'MEMORY' || focus === 'RAW';
const jtext = States.useRequest(TIP.printSequent, {
- node,
- iformat,
- rformat,
- autofocus,
- unmangled,
+ node, iformat, rformat, autofocus, unmangled,
}) ?? null;
+ const { part, term } = States.useRequest(TIP.getSelection, node) ?? {};
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]
+ );
const [hover, setHover] = React.useState<Decorations>(null);
const onHover = React.useCallback((pos: Position | null) => {
- if (pos) {
- const { step, term } = sequent.locate(pos.offset);
- const range = term ?? step;
- if (range) {
- const { offset, endOffset } = range;
- const length = endOffset - offset;
- setHover({ className: 'cm-hovered-code', offset, length });
- return;
+ setHover(sequent.hover(pos));
+ }, [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;
+ }
}
}
- setHover(null);
- }, [sequent]);
+ Server.send(TIP.clearSelection, node);
+ }, [sequent, node]);
return (
<TextView
readOnly
text={sequent.text}
+ selection={selection}
decorations={[hover, sequent.decorations]}
onHover={onHover}
+ onClick={onClick}
/>
);
}
diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx
index 3e8c65b6cbde11c80cbe07fd5924262cfc4fbb5f..2fd37ff7ce138fda8ae9c13e454d90af87d7b65b 100644
--- a/ivette/src/frama-c/richtext.tsx
+++ b/ivette/src/frama-c/richtext.tsx
@@ -61,8 +61,13 @@ export type Tag = {
endOffset: number,
children: Tags
};
+
export type TagIndex = Map<string, Tags>;
+export function contains(a: Tag, b: Tag): boolean {
+ return a.offset <= b.offset && b.endOffset <= a.endOffset;
+}
+
/** Extract a Tag forest from a text. */
export function textToTags(
text: KernelData.text,
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 6ed15dd834f470ddd7613633c53be71018da5fb9..256d87982b99c0a9ffe972dd30d9db65fcd2e377 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -367,7 +367,9 @@ let () =
~output:(module D.Junit)
begin fun node ->
let pp = lookup_printer node in
- pp#reset ; R.emit printStatus
+ pp#reset ;
+ pp#selected ;
+ R.emit printStatus
end
let () =
@@ -397,4 +399,22 @@ let () =
R.emit printStatus
end
+let () =
+ let getSelection = R.signature ~input:(module Node) () in
+ let set_part = R.result_opt getSelection ~name:"part"
+ ~descr:(Md.plain "Selected part") (module Part) in
+ let set_term = R.result_opt getSelection ~name:"term"
+ ~descr:(Md.plain "Selected term") (module Term) in
+ R.register_sig ~package
+ ~kind:`GET
+ ~name:"getSelection"
+ ~descr:(Md.plain "Get current selection in proof node")
+ ~signals:[printStatus]
+ getSelection
+ begin fun rq node ->
+ let (part,term) = (lookup_printer node)#target in
+ set_part rq (if part <> Term then Some (of_part part) else None);
+ set_term rq term;
+ end
+
(* -------------------------------------------------------------------------- *)