diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index ea0adb0a322003ad704ce492e4c713c73c1deaf0..f08e710e7cd49a91ed317a46e8c75bff5a941290 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -38,6 +38,25 @@ import { IconButton } from 'dome/controls/buttons';
import * as Boxes from 'dome/layout/boxes';
import { TitleBar } from 'ivette';
+// --------------------------------------------------------------------------
+// --- Marker Utility
+// --------------------------------------------------------------------------
+
+function addMarker(
+ ms: AST.marker[],
+ m: AST.marker | undefined
+): AST.marker[] {
+ return m ? (ms.includes(m) ? ms : ms.concat(m)) : ms;
+}
+
+function toggleMarker(ms: AST.marker[], m: AST.marker): AST.marker[] {
+ return ms.includes(m) ? ms.filter((m0) => m0 !== m) : ms.concat(m);
+}
+
+function makeFilter(filter: string): string[] {
+ return filter.split('').filter((s) => s.length > 0).sort();
+}
+
// --------------------------------------------------------------------------
// --- Marker Kinds
// --------------------------------------------------------------------------
@@ -79,81 +98,110 @@ function markerKind(props: AST.markerInfoData): JSX.Element {
// --- Information Details
// --------------------------------------------------------------------------
-interface InfoItemProps {
- label: string;
- title: string;
+interface FieldInfo {
+ id: string;
+ label: string; // short name
+ title: string; // long titled name
+ descr: string; // information value long description
text: DATA.text;
- onMarker: (m: AST.marker) => void;
}
-function InfoItem(props: InfoItemProps): JSX.Element {
- const onMarker = (m: string) => void props.onMarker(AST.jMarker(m));
+interface FieldInfoProps {
+ field: FieldInfo;
+ onSelected: (m: AST.marker) => void;
+ onHovered: (m: AST.marker | undefined) => void;
+}
+
+function FieldInfo(props: FieldInfoProps): JSX.Element {
+ const onSelected = (m: string) => void props.onSelected(AST.jMarker(m));
+ const onHovered = (m: string | undefined): void => {
+ props.onHovered(m ? AST.jMarker(m) : undefined);
+ };
+ const { label, descr, title, text } = props.field;
return (
- <div className="astinfo-infos">
- <div className="dome-text-label astinfo-kind" title={props.title}>
- {props.label}
+ <div className="astinfo-infos" >
+ <div className="dome-text-label astinfo-kind" title={title}>
+ {label}
</div>
- <div className="dome-text-cell astinfo-data" title={props.title}>
- <Text onMarker={onMarker} text={props.text} />
+ <div className="dome-text-cell astinfo-data" title={descr}>
+ <Text onSelected={onSelected} onHovered={onHovered} text={text} />
</div>
- </div>
+ </div >
);
}
-interface ASTinfos {
- id: string;
- label: string;
- descr: string;
+// --------------------------------------------------------------------------
+// --- Mark Informations Buttons
+// --------------------------------------------------------------------------
+
+interface MarkButtonProps {
+ icon: string;
title: string;
- text: DATA.text;
+ visible?: boolean;
+ display?: boolean;
+ selected?: boolean;
+ onClick: () => void;
+}
+
+function MarkButton(props: MarkButtonProps): JSX.Element {
+ return (
+ <IconButton
+ className="astinfo-markerbutton"
+ size={10}
+ offset={0}
+ {...props}
+ />
+ );
}
+// --------------------------------------------------------------------------
+// --- Mark Informations Section
+// --------------------------------------------------------------------------
+
interface InfoSectionProps {
+ scroll: React.RefObject<HTMLDivElement> | undefined;
marker: AST.marker;
- markerInfo: AST.markerInfoData;
- filter: string;
- selected: boolean;
- hovered: boolean;
- pinned: boolean;
- onPin: () => void;
- onHover: (hover: boolean) => void;
- onSelect: () => void;
- onRemove: () => void;
- onMarker: (m: AST.marker) => void;
+ markerInfos: AST.markerInfoData;
+ scrolled: AST.marker | undefined;
+ selected: AST.marker | undefined;
+ hovered: AST.marker | undefined;
+ marked: boolean;
+ excluded: string[];
+ onHovered: (m: AST.marker | undefined) => void;
+ onFocused: (m: AST.marker | undefined) => void; // internal hover
+ onSelected: (m: AST.marker) => void;
+ onPinned: (m: AST.marker) => void;
+ onChildSelected: (m: AST.marker, e: AST.marker) => void;
}
function MarkInfos(props: InfoSectionProps): JSX.Element {
+ const { marker, markerInfos } = props;
+ const { scrolled, selected, hovered, excluded } = props;
const [unfold, setUnfold] = React.useState(true);
- const [more, setMore] = React.useState(false);
- const { marker: m, markerInfo } = props;
- const req = React.useMemo(() => Server.send(AST.getInformation, m), [m]);
- const { result: allInfos = [] } = Dome.usePromise(req);
+ const [expand, setExpand] = React.useState(false);
+ const req = React.useMemo(() => Server.send(AST.getInformation, marker), [marker]);
+ const { result: markerFields = [] } = Dome.usePromise(req);
+ const isScrolled = marker === scrolled;
+ const isHovered = marker === hovered;
+ const isSelected = marker === selected;
const highlight = classes(
- props.selected && 'selected',
- props.hovered && 'hovered',
+ isSelected && 'selected',
+ isHovered && 'hovered',
);
- const kind = markerKind(markerInfo);
- const name = markerInfo.name;
- const descr = markerInfo.descr ?? `${kind} ${name}`;
- const fs = props.filter.split(':');
- const filtered = allInfos.filter((info) => !fs.some((m) => m === info.id));
- const infos = more ? allInfos : filtered;
- const hasMore = filtered.length < allInfos.length;
- const pinButton =
- (!props.pinned || props.selected) ?
- {
- icon: "PIN", selected: props.pinned, onClick: props.onPin,
- title: "Pin/unpin marker information"
- } : {
- icon: "CIRC.CLOSE", onClick: props.onRemove,
- title: "Remove marker information"
- };
+ const kind = markerKind(markerInfos);
+ const name = markerInfos.name;
+ const descr = markerInfos.descr ?? `${kind} ${name}`;
+ const filtered = markerFields.filter((fd) => !excluded.includes(fd.id));
+ const hasMore = filtered.length < markerFields.length;
+ const displayed = expand ? markerFields : filtered;
+ const onSelected = (m: AST.marker): void => props.onChildSelected(marker, m);
return (
<div
+ ref={isScrolled ? props.scroll : undefined}
className={`astinfo-section ${highlight}`}
- onMouseEnter={() => props.onHover(true)}
- onMouseLeave={() => props.onHover(false)}
- onDoubleClick={props.onSelect}
+ onMouseEnter={() => props.onHovered(marker)}
+ onMouseLeave={() => props.onHovered(undefined)}
+ onDoubleClick={() => props.onSelected(marker)}
>
<div
key="MARKER"
@@ -161,223 +209,169 @@ function MarkInfos(props: InfoSectionProps): JSX.Element {
title={descr}
>
<Icon
+ key="FOLDER"
className="astinfo-folderbutton"
- style={{ visibility: infos.length ? 'visible' : 'hidden' }}
- size={9}
+ visible={displayed.length > 0}
+ size={10}
offset={-2}
id={unfold ? 'TRIANGLE.DOWN' : 'TRIANGLE.RIGHT'}
onClick={() => setUnfold(!unfold)}
/>
- <Code className="astinfo-markercode">
- {kind}{name}
+ <Code key="NAME" className="astinfo-markercode">
+ {kind} {name}
</Code>
- <IconButton
- style={{ display: hasMore ? undefined : 'none' }}
- className="astinfo-markerbutton"
- title="Show all available information"
- size={9}
- offset={0}
+ <MarkButton
+ key="MORE"
icon="CIRC.PLUS"
- selected={more}
- onClick={() => setMore(!more)}
+ display={hasMore}
+ title="Show all available information"
+ selected={expand}
+ onClick={() => setExpand(!expand)}
/>
- <IconButton
- className="astinfo-markerbutton"
- size={9}
- offset={0}
- {...pinButton}
+ <MarkButton
+ key="PIN"
+ icon="PIN"
+ selected={props.marked}
+ display={props.marked || isSelected || !isHovered}
+ title="Remove Information"
+ onClick={() => props.onPinned(marker)}
/>
</div>
- {unfold && infos.map((info) => (
- <InfoItem key={info.id} onMarker={props.onMarker} {...info} />
+ {unfold && displayed.map((field) => (
+ <FieldInfo
+ key={field.id}
+ field={field}
+ onHovered={props.onFocused}
+ onSelected={onSelected}
+ />
))}
</div>
);
}
-// --------------------------------------------------------------------------
-// --- Information Selection State
-// --------------------------------------------------------------------------
-
-type Mark = { fct: string; marker: AST.marker };
-
-const reload = new Dome.Event('frama-c.astinfo');
-
-function addMarker(s: Mark[], marker: AST.marker, fct: string): Mark[] {
- if (s.some((m) => m.marker === marker))
- return s;
- else
- return s.concat({ marker, fct });
-}
-
-class InfoMarkers {
-
- private selection: Mark[] = [];
- private mSelected: AST.marker | undefined;
- private mHovered: AST.marker | undefined;
- private pinned = new Set<string>();
-
- isPinned(marker: AST.marker): boolean {
- return this.pinned.has(marker);
- }
-
- setPinned(marker: AST.marker, pinned: boolean): void {
- const oldpin = this.isPinned(marker);
- if (oldpin !== pinned) {
- if (pinned)
- this.pinned.add(marker);
- else
- this.pinned.delete(marker);
- reload.emit();
- }
- }
-
- setLocations(
- selected: States.Location | undefined,
- hovered: States.Location | undefined
- ): void {
- const sm = selected?.marker;
- const sf = selected?.fct;
- const hm = hovered?.marker;
- const hf = hovered?.fct;
- const s0 = this.mSelected;
- const h0 = this.mHovered;
- let s = this.selection.filter((mark): boolean => {
- const m = mark.marker;
- return this.isPinned(m) || (m !== s0 && m !== h0);
- });
- if (sm && sf) s = addMarker(s, sm, sf);
- if (hm && hf) s = addMarker(s, hm, hf);
- this.selection = s;
- this.mSelected = sm;
- this.mHovered = hm;
- reload.emit();
- }
-
- removeMarker(marker: AST.marker): void {
- if (marker === this.mSelected) this.mSelected = undefined;
- if (marker === this.mHovered) this.mHovered = undefined;
- this.selection = this.selection.filter((m) => m.marker !== marker);
- this.pinned.delete(marker);
- reload.emit();
- }
-
- getSelected(): Mark[] { return this.selection; }
-
-}
-
// --------------------------------------------------------------------------
// --- Context Menu Filter
// --------------------------------------------------------------------------
function openFilter(
- infos: ASTinfos[],
- filter: string,
- onChange: (f: string) => void,
+ fields: FieldInfo[],
+ excluded: string[],
+ onChange: (filter: string[]) => void,
): void {
- const fs = filter.split(':');
- const menuItems = infos.map((info) => {
- const checked = !fs.some((m) => m === info.id);
+ const menuItem = (fd: FieldInfo): Dome.PopupMenuItem => {
+ const checked = !excluded.includes(fd.id);
const onClick = (): void => {
- const newFs =
+ const newFilter =
checked
- ? fs.concat(info.id)
- : fs.filter((m) => m !== info.id);
- onChange(newFs.join(':'));
+ ? excluded.concat(fd.id)
+ : excluded.filter((m) => m !== fd.id);
+ onChange(newFilter);
};
return {
- id: info.id,
- label: `${info.descr} (${info.label})`,
+ id: fd.id,
+ label: `${fd.title} (${fd.label})`,
checked,
onClick,
};
- });
- Dome.popupMenu(menuItems);
- return;
+ };
+ Dome.popupMenu(fields.map(menuItem));
}
// --------------------------------------------------------------------------
// --- Information Panel
// --------------------------------------------------------------------------
+const filterSettings = 'frama-c.sidebar.astinfo.filter';
+
export default function ASTinfo(): JSX.Element {
// Hooks
- Dome.useUpdate(reload);
- const markers = React.useMemo(() => new InfoMarkers(), []);
- const markerInfos = States.useSyncArray(AST.markerInfo, false);
+ const [markers, setMarkers] = React.useState<AST.marker[]>([]);
+ const [setting, setSetting] = Dome.useStringSettings(filterSettings, '');
const [selection, setSelection] = States.useSelection();
- const [hoveredLoc] = States.useHovered();
- const information = States.useRequest(AST.getInformation, null) ?? [];
- const [filter, setFilter] =
- Dome.useStringSettings('frama-c.sidebar.astinfo.filter', '');
- const selectedLoc = selection?.current;
- const selected = selectedLoc?.marker;
- const hovered = hoveredLoc?.marker;
- React.useEffect(() => {
- markers.setLocations(selectedLoc, hoveredLoc);
- }, [markers, selectedLoc, hoveredLoc]);
- const pinMarker = React.useCallback((location: States.Location) => {
- if (location?.marker)
- markers.setPinned(location?.marker, true);
- }, [markers]);
- React.useEffect(() => {
- States.MetaSelection.on(pinMarker);
- return () => States.MetaSelection.off(pinMarker);
- }, [pinMarker]);
- const scrollTarget = React.useRef<HTMLInputElement>(null);
+ const [hovering] = States.useHovered();
+ const [focused, setFocused] = React.useState<AST.marker | undefined>();
+ const allInfos = States.useSyncArray(AST.markerInfo);
+ const allFields = States.useRequest(AST.getInformation, null) ?? [];
+ const scroll = React.useRef<HTMLDivElement>(null);
+ const excluded = React.useMemo(() => makeFilter(setting), [setting]);
React.useEffect(() => {
- scrollTarget.current?.scrollIntoView({ block: 'nearest' });
+ scroll.current?.scrollIntoView({ block: 'nearest' });
});
- // Rendering
- const renderMark = (mark: Mark): JSX.Element | null => {
- const { marker } = mark;
- const markerInfo = markerInfos.getData(marker);
- if (!markerInfo) return null;
- const pinned = markers.isPinned(marker);
- const isSelected = selected === marker;
- const isHovered = hovered === marker;
- const onPin = () => void markers.setPinned(marker, !pinned);
- const onRemove = () => void markers.removeMarker(marker);
- const onSelect = () => void States.setSelection(mark);
- const onHover =
- (h: boolean): void => States.setHovered(h ? mark : undefined);
- const onMarker =
- (marker: AST.marker): void => {
- const fct = selection?.current?.fct;
- if (fct) {
- markers.setPinned(marker, true);
- setSelection({ location: { fct, marker } });
- }
- };
- const ref = isHovered ? scrollTarget : undefined;
- const markInfo =
+ // Derived
+ const fct = selection?.current?.fct;
+ const selected = selection?.current?.marker;
+ const hovered = hovering?.marker;
+ const allMarkers = addMarker(addMarker(markers, selected), hovered);
+ const scrolled = focused === hovered ? undefined : (hovered || selected);
+ // Callbacks
+ const setExcluded = (fs: string[]): void =>
+ setSetting(fs.join(':'));
+ const onSelected = (marker: AST.marker): void =>
+ setSelection({ location: { fct, marker } });
+ const onHovered = (marker: AST.marker | undefined): void => {
+ States.setHovered(marker ? { fct, marker } : undefined);
+ };
+ const onFocused = (marker: AST.marker | undefined): void => {
+ onHovered(marker);
+ setFocused(marker);
+ };
+ const onPinned = (m: AST.marker): void =>
+ setMarkers(toggleMarker(markers, m));
+ const onChildSelected = (m: AST.marker, e: AST.marker): void => {
+ setMarkers(addMarker(markers, m));
+ setFocused(undefined);
+ onSelected(e);
+ };
+ // Mark Rendering
+ const renderMark = (marker: AST.marker): JSX.Element | null => {
+ const markerInfos = allInfos.getData(marker);
+ if (!markerInfos) return null;
+ return (
<MarkInfos
key={marker}
+ scroll={scroll}
marker={marker}
- markerInfo={markerInfo}
- pinned={pinned}
- selected={isSelected}
- filter={filter}
- hovered={isHovered}
- onPin={onPin}
- onMarker={onMarker}
- onRemove={onRemove}
- onHover={onHover}
- onSelect={onSelect}
- />;
- return <div ref={ref}>{markInfo}</div>;
+ markerInfos={markerInfos}
+ scrolled={scrolled}
+ hovered={hovered}
+ selected={selected}
+ excluded={excluded}
+ marked={markers.includes(marker)}
+ onSelected={onSelected}
+ onHovered={onHovered}
+ onFocused={onFocused}
+ onPinned={onPinned}
+ onChildSelected={onChildSelected}
+ />
+ );
};
+ // Information Panel Rendering
return (
<>
<TitleBar>
<IconButton
+ key="CLEAR"
+ icon="CIRC.CLOSE"
+ title="Clear Information Panel"
+ display={markers.length > 0}
+ onClick={() => setMarkers([])}
+ />
+ <IconButton
+ key="RESET"
+ icon="CIRC.PLUS"
+ title="Reset Information Filter"
+ display={excluded.length > 0}
+ onClick={() => setSetting('')}
+ />
+ <IconButton
+ key="FILTER"
icon="CLIPBOARD"
- onClick={() => openFilter(information, filter, setFilter)}
title="Information Filters"
+ onClick={() => openFilter(allFields, excluded, setExcluded)}
/>
</TitleBar>
<Boxes.Scroll>
- {React.Children.toArray(markers.getSelected().map(renderMark))}
+ {allMarkers.map(renderMark)}
</Boxes.Scroll>
</>
);
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 765167a4084cecb31a45fe78a86076d1c05c242b..d9e379b69bb3854a030fb87aaa4e9e16713d2346 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -429,7 +429,7 @@ export const getInformationUpdate: Server.Signal = {
const getInformation_internal: Server.GetRequest<
marker |
undefined,
- { id: string, label: string, descr: string, title: string, text: text }[]
+ { id: string, label: string, title: string, descr: string, text: text }[]
> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getInformation',
@@ -438,8 +438,8 @@ const getInformation_internal: Server.GetRequest<
Json.jObject({
id: Json.jString,
label: Json.jString,
- descr: Json.jString,
title: Json.jString,
+ descr: Json.jString,
text: jText,
})),
signals: [ { name: 'kernel.ast.getInformationUpdate' } ],
@@ -448,7 +448,7 @@ const getInformation_internal: Server.GetRequest<
export const getInformation: Server.GetRequest<
marker |
undefined,
- { id: string, label: string, descr: string, title: string, text: text }[]
+ { id: string, label: string, title: string, descr: string, text: text }[]
>= getInformation_internal;
const getMarkerAt_internal: Server.GetRequest<
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index 256a011ab9364c33993696d9b496f52a77cc8a92..7d60d1862dfbde46ba35a1a3ffdadc2e12938c8b 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -128,6 +128,8 @@
.astinfo-markerbutton {
flex: 0 1 auto;
margin: 0px;
+ padding-left: 4px;
+ padding-right: 4px;
position: relative;
}
diff --git a/ivette/src/frama-c/richtext.tsx b/ivette/src/frama-c/richtext.tsx
index f819ccae1521d4619a1b9a814310ff97bdfa84fd..c129f601d870e8a6bfecae9dbdabea650404550f 100644
--- a/ivette/src/frama-c/richtext.tsx
+++ b/ivette/src/frama-c/richtext.tsx
@@ -77,17 +77,19 @@ export function printTextWithTags(
interface MarkerProps {
marker: string;
- onMarker?: (marker: string) => void;
+ onSelected?: (marker: string) => void;
+ onHovered?: (marker: string | undefined) => void;
children?: React.ReactNode;
}
function Marker(props: MarkerProps): JSX.Element {
- const { marker, onMarker, children } = props;
- const onClick = (): void => { if (onMarker) onMarker(marker); };
+ const { marker, onSelected, onHovered, children } = props;
return (
<span
className="kernel-text-marker"
- onClick={onClick}
+ onClick={() => onSelected && onSelected(marker)}
+ onMouseEnter={() => onHovered && onHovered(marker)}
+ onMouseLeave={() => onHovered && onHovered(undefined)}
>
{children}
</span>
@@ -96,7 +98,8 @@ function Marker(props: MarkerProps): JSX.Element {
export interface TextProps {
text: KernelData.text;
- onMarker?: (marker: string) => void;
+ onSelected?: (marker: string) => void;
+ onHovered?: (marker: string | undefined) => void;
className?: string;
}
@@ -110,7 +113,11 @@ export function Text(props: TextProps): JSX.Element {
const contents = React.Children.toArray(array.map(makeContents));
if (marker) {
return (
- <Marker marker={tag} onMarker={props.onMarker}>
+ <Marker
+ marker={tag}
+ onSelected={props.onSelected}
+ onHovered={props.onHovered}
+ >
{contents}
</Marker>
);
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 216313063866d220a8376240db8ee9fdf02153a7..fede8dc75f586e54ea148ed53db04eb204d2e6d2 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -222,7 +222,7 @@ let () =
Server.Kernel_ast.Information.register
~id:"eva.value"
~label:"Value"
- ~descr:"Possible values inferred by Eva"
+ ~title:"Possible values inferred by Eva"
~enable:Analysis.is_computed
print_value
@@ -275,7 +275,7 @@ module EvaTaints = struct
if before = after then Format.fprintf fmt "%a" pretty before
else Format.fprintf fmt "Before: %a@\nAfter: %a" pretty before pretty after
- let eva_taints_title =
+ let eva_taints_descr =
"Taint status:\n\
- Direct taint: data dependency from values provided by the attacker, \
meaning that the attacker may be able to alter this value\n\
@@ -287,8 +287,8 @@ module EvaTaints = struct
let taint_computed = Taint_domain.Store.is_computed in
let enable () = Analysis.is_computed () && taint_computed () in
Server.Kernel_ast.Information.register
- ~id:"eva.taint" ~label:"Taint" ~descr: "Taint status according to Eva"
- ~title:eva_taints_title ~enable print_taint
+ ~id:"eva.taint" ~label:"Taint" ~title: "Taint status according to Eva"
+ ~descr:eva_taints_descr ~enable print_taint
let update = Server.Kernel_ast.Information.update
let () = Analysis.register_computation_hook (fun _ -> update ())
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 9b79cf916cfcf82a4810e36bf4eeb39215eacf64..82c153f1e9a7b1c18524a5746d6c3eb7c330685a 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -583,9 +583,9 @@ struct
type info = {
id: string;
rank: int;
- label: string;
- descr: string;
- title: string;
+ label: string; (* short name *)
+ title: string; (* full title name *)
+ descr: string; (* description for information values *)
enable: unit -> bool;
pretty: Format.formatter -> Printer_tag.localizable -> unit
}
@@ -598,16 +598,16 @@ struct
let jtype = Package.(Jrecord[
"id", Jstring ;
"label", Jstring ;
- "descr", Jstring ;
"title", Jstring ;
+ "descr", Jstring ;
"text", Jtext.jtype ;
])
let of_json _ = failwith "Information.Info"
let to_json (info,text) = `Assoc [
"id", `String info.id ;
"label", `String info.label ;
- "descr", `String info.descr ;
"title", `String info.title ;
+ "descr", `String info.descr ;
"text", text ;
]
end
@@ -650,11 +650,12 @@ struct
let update () = Request.emit signal
- let register ~id ~label ~descr
- ?(title = descr)
- ?(enable = fun _ -> true) pretty =
+ let register ~id ~label ~title
+ ?(descr = title)
+ ?(enable = fun _ -> true)
+ pretty =
let rank = incr rankId ; !rankId in
- let info = { id ; rank ; label ; descr; title ; enable ; pretty } in
+ let info = { id ; rank ; label ; title ; descr; enable ; pretty } in
if Hashtbl.mem registry id then
( let msg = Format.sprintf
"Server.Kernel_ast.register_info: duplicate %S" id in
@@ -681,16 +682,18 @@ let () = Request.register ~package
let () = Information.register
~id:"kernel.ast.location"
~label:"Location"
- ~descr:"Source file location"
+ ~title:"Source file location"
begin fun fmt loc ->
- let location = Printer_tag.loc_of_localizable loc in
- Filepath.pp_pos fmt (fst location)
+ let pos = fst @@ Printer_tag.loc_of_localizable loc in
+ if Filepath.Normalized.is_empty pos.pos_path then
+ raise Not_found ;
+ Filepath.pp_pos fmt pos
end
let () = Information.register
~id:"kernel.ast.varinfo"
~label:"Var"
- ~descr:"Variable Information"
+ ~title:"Variable Information"
begin fun fmt loc ->
match loc with
| PLval (_ , _, (Var x,NoOffset)) | PVDecl(_,_,x) ->
@@ -714,7 +717,7 @@ let () = Information.register
let () = Information.register
~id:"kernel.ast.typeinfo"
~label:"Type"
- ~descr:"Type of C/ASCL expression"
+ ~title:"Type of C/ASCL expression"
begin fun fmt loc ->
let open Printer in
match loc with
@@ -728,7 +731,7 @@ let () = Information.register
let () = Information.register
~id:"kernel.ast.typedef"
~label:"Typedef"
- ~descr:"Type Definition"
+ ~title:"Type Definition"
begin fun fmt loc ->
match loc with
| PGlobal
@@ -742,7 +745,7 @@ let () = Information.register
let () = Information.register
~id:"kernel.ast.typesizeof"
~label:"Sizeof"
- ~descr:"Size of a C type"
+ ~title:"Size of a C type"
begin fun fmt loc ->
let typ =
match loc with
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 1ffebc5e66f6ddbe69dc5f8b7d7ab047b3e862cc..938b968119c75c8cde64956550670142f15da074 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -72,16 +72,17 @@ sig
(**
Registers a marker information printer.
Identifier [id] shall be unique.
- [label] shall be very short.
- [descr] shall succinctly describe the kind of information.
- [title] is an optional longer explanation for the kind of information.
- If the optional [enable] function is provided, the information printer is
- only used when [enable ()] returns true.
- The printer is allowed to raise [Not_found] exception when there is no
+
+ - [label] shall be very short.
+ - [title] shall succinctly describe the kind of information.
+ - [descr] optional longer description explaining the informations
+ - [enable] optional dynamical filter for enabling this information
+
+ The printer shall raise [Not_found] exception when there is no
information for the localizable.
*)
val register :
- id:string -> label:string -> descr:string -> ?title:string ->
+ id:string -> label:string -> title:string -> ?descr:string ->
?enable:(unit -> bool) ->
(Format.formatter -> Printer_tag.localizable -> unit) -> unit