Skip to content
Snippets Groups Projects
Commit 9d8d7c42 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[ivette/wp] refactor tip files

parent aaaa1a47
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ivette/src/frama-c/plugins/wp/seq.tsx 0 → 100644
+ 209
− 0
View file @ 9d8d7c42
/* ************************************************************************ */
/* */
/* 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). */
/* */
/* ************************************************************************ */
import React from 'react';
import { jOption } from 'dome/data/json';
import {
MarkDecoration, GutterDecoration, Decorations,
Position, Range, TextProxy, 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';
import * as TIP from 'frama-c/plugins/wp/api/tip';
/* -------------------------------------------------------------------------- */
/* --- Sequent Decorations --- */
/* -------------------------------------------------------------------------- */
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;
private readonly tags: RichText.Tags;
private readonly style: MarkDecoration[];
private readonly index: RichText.TagIndex;
constructor(jtext: text) {
this.contents = RichText.textToString(jtext);
this.style = [];
const addStyle = (tg: RichText.Tag, className: string): void => {
const { offset, endOffset } = tg;
const length = endOffset - offset;
this.style.push({ className, offset, length });
};
const filter = (t: RichText.Tag): boolean => {
switch(t.tag) {
case 'wp:comment':
case 'wp:property':
addStyle(t, 'cm-comment');
return false;
case 'wp:stmt':
case 'wp:clause':
case 'wp:warning':
addStyle(t, 'cm-keyword');
return false;
case 'wp:label':
addStyle(t, 'cm-def');
return false;
case 'wp:var':
addStyle(t, 'cm-type');
return false;
case 'wp:focus':
addStyle(t, 'cm-multiple-code');
return false;
case 'wp:target':
addStyle(t, 'cm-selected-code');
return false;
}
return t.tag.startsWith('#');
};
const { index, tags } = RichText.textToTags(jtext, filter);
this.tags = tags;
this.index = index;
}
get text(): string {
return this.contents;
}
get decorations(): Decorations {
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];
}
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');
};
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;
}
}
/* -------------------------------------------------------------------------- */
/* --- Sequent View --- */
/* -------------------------------------------------------------------------- */
export interface GoalViewProps {
node: Node;
autofocus: boolean;
unmangled: boolean;
iformat: TIP.iformat;
rformat: TIP.rformat;
}
export function GoalView(props: GoalViewProps): JSX.Element {
const { node } = props;
const jtext = States.useRequest(TIP.printSequent, props, {
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]);
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) => {
setHover(sequent.hover(pos));
}, [sequent]);
const onClick = React.useCallback((pos: Position | null) => {
setHover(null);
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);
}, [sequent, node]);
return (
<TextView
readOnly
className='wp'
text={proxy}
selection={selection}
decorations={[hover, sequent.decorations, gutters]}
onHover={onHover}
onClick={onClick}
/>
);
}
/* -------------------------------------------------------------------------- */
ivette/src/frama-c/plugins/wp/tip.tsx
+ 7
− 186
View file @ 9d8d7c42
...@@ -23,23 +23,16 @@ ...@@ -23,23 +23,16 @@
import React from 'react'; import React from 'react';
import * as Dome from 'dome'; import * as Dome from 'dome';
import { jOption, json } from 'dome/data/json'; import { json } from 'dome/data/json';
import { Cell } from 'dome/controls/labels'; import { Cell } from 'dome/controls/labels';
import { ToolBar, Select, Filler } from 'dome/frame/toolbars'; import { ToolBar, Select, Filler } from 'dome/frame/toolbars';
import { Vfill } from 'dome/layout/boxes'; import { Vfill } from 'dome/layout/boxes';
import {
MarkDecoration, GutterDecoration, Decorations,
Position, Range, TextProxy, TextView,
} from 'dome/text/richtext';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states'; import * as States from 'frama-c/states';
import * as RichText from 'frama-c/richtext';
import type { text } from 'frama-c/kernel/api/data';
import * as WP from 'frama-c/plugins/wp/api'; import * as WP from 'frama-c/plugins/wp/api';
import * as TIP from 'frama-c/plugins/wp/api/tip'; import * as TIP from 'frama-c/plugins/wp/api/tip';
import { getStatus } from './goals'; import { getStatus } from './goals';
import { GoalView } from './seq';
/* -------------------------------------------------------------------------- */ /* -------------------------------------------------------------------------- */
/* --- Sequent Printing Modes --- */ /* --- Sequent Printing Modes --- */
...@@ -110,187 +103,12 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element { ...@@ -110,187 +103,12 @@ function RFormatSelector(props: Selector<TIP.rformat>): JSX.Element {
); );
} }
/* -------------------------------------------------------------------------- */
/* --- Sequent Decorations --- */
/* -------------------------------------------------------------------------- */
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;
private readonly tags: RichText.Tags;
private readonly style: MarkDecoration[];
private readonly index: RichText.TagIndex;
constructor(jtext: text) {
this.contents = RichText.textToString(jtext);
this.style = [];
const addStyle = (tg: RichText.Tag, className: string): void => {
const { offset, endOffset } = tg;
const length = endOffset - offset;
this.style.push({ className, offset, length });
};
const filter = (t: RichText.Tag): boolean => {
switch(t.tag) {
case 'wp:comment':
case 'wp:property':
addStyle(t, 'cm-comment');
return false;
case 'wp:stmt':
case 'wp:clause':
case 'wp:warning':
addStyle(t, 'cm-keyword');
return false;
case 'wp:label':
addStyle(t, 'cm-def');
return false;
case 'wp:var':
addStyle(t, 'cm-type');
return false;
case 'wp:focus':
addStyle(t, 'cm-multiple-code');
return false;
case 'wp:target':
addStyle(t, 'cm-selected-code');
return false;
}
return t.tag.startsWith('#');
};
const { index, tags } = RichText.textToTags(jtext, filter);
this.tags = tags;
this.index = index;
}
get text(): string {
return this.contents;
}
get decorations(): Decorations {
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];
}
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');
};
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;
}
}
/* -------------------------------------------------------------------------- */
/* --- Sequent View --- */
/* -------------------------------------------------------------------------- */
interface GoalViewProps {
node: Node;
focus: Focus;
iformat: TIP.iformat;
rformat: TIP.rformat;
}
function GoalView(props: GoalViewProps): JSX.Element {
const { node, focus, iformat, rformat } = props;
const autofocus = focus === 'AUTOFOCUS' || focus === 'MEMORY';
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]);
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) => {
setHover(sequent.hover(pos));
}, [sequent]);
const onClick = React.useCallback((pos: Position | null) => {
setHover(null);
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);
}, [sequent, node]);
return (
<TextView
readOnly
className='wp'
text={proxy}
selection={selection}
decorations={[hover, sequent.decorations, gutters]}
onHover={onHover}
onClick={onClick}
/>
);
}
/* -------------------------------------------------------------------------- */ /* -------------------------------------------------------------------------- */
/* --- TIP View --- */ /* --- TIP View --- */
/* -------------------------------------------------------------------------- */ /* -------------------------------------------------------------------------- */
interface ProofState { interface ProofState {
current: Node; current: TIP.node | undefined;
index: number; index: number;
pending: number; pending: number;
} }
...@@ -328,6 +146,8 @@ export function TIPView(props: TIPProps): JSX.Element { ...@@ -328,6 +146,8 @@ export function TIPView(props: TIPProps): JSX.Element {
const [ rformat, setRformat ] = Dome.useWindowSettings<TIP.rformat>( const [ rformat, setRformat ] = Dome.useWindowSettings<TIP.rformat>(
'wp.tip.rformat', TIP.jRformat, 'ratio' 'wp.tip.rformat', TIP.jRformat, 'ratio'
); );
const autofocus = focus === 'AUTOFOCUS' || focus === 'MEMORY';
const unmangled = focus === 'MEMORY' || focus === 'RAW';
return ( return (
<Vfill display={display}> <Vfill display={display}>
<ToolBar> <ToolBar>
...@@ -346,7 +166,8 @@ export function TIPView(props: TIPProps): JSX.Element { ...@@ -346,7 +166,8 @@ export function TIPView(props: TIPProps): JSX.Element {
</ToolBar> </ToolBar>
<GoalView <GoalView
node={current} node={current}
focus={focus} autofocus={autofocus}
unmangled={unmangled}
iformat={iformat} iformat={iformat}
rformat={rformat} rformat={rformat}
/> />
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment