diff --git a/ivette/src/dome/renderer/controls/gallery.json b/ivette/src/dome/renderer/controls/gallery.json
index 719e0b838040aa67305e87be0730254a02810214..efae6ebd9938395b4f9028873133d3e3c4689b80 100644
--- a/ivette/src/dome/renderer/controls/gallery.json
+++ b/ivette/src/dome/renderer/controls/gallery.json
@@ -325,6 +325,18 @@
"viewBox": "0 0 16 16",
"path": "M16 0h-6.5l2.5 2.5-3 3 1.5 1.5 3-3 2.5 2.5z M16 16v-6.5l-2.5 2.5-3-3-1.5 1.5 3 3-2.5 2.5z M0 16h6.5l-2.5-2.5 3-3-1.5-1.5-3 3-2.5-2.5z M0 0v6.5l2.5-2.5 3 3 1.5-1.5-3-3 2.5-2.5z"
},
+ "CHEVRON.CONTRACT": {
+ "section": "Arrows",
+ "title": "Chevron.contract",
+ "viewBox": "0 0 16 16",
+ "path": "M3.646 13.854a.5.5 0 0 0 .708 0L8 10.207l3.646 3.647a.5.5 0 0 0 .708-.708l-4-4a.5.5 0 0 0-.708 0l-4 4a.5.5 0 0 0 0 .708zm0-11.708a.5.5 0 0 1 .708 0L8 5.793l3.646-3.647a.5.5 0 0 1 .708.708l-4 4a.5.5 0 0 1-.708 0l-4-4a.5.5 0 0 1 0-.708z"
+ },
+ "CHEVRON.EXPAND": {
+ "section": "Arrows",
+ "title": "Chevron.expand",
+ "viewBox": "0 0 16 16",
+ "path": "M3.646 9.146a.5.5 0 0 1 .708 0L8 12.793l3.646-3.647a.5.5 0 0 1 .708.708l-4 4a.5.5 0 0 1-.708 0l-4-4a.5.5 0 0 1 0-.708zm0-2.292a.5.5 0 0 0 .708 0L8 3.207l3.646 3.647a.5.5 0 0 0 .708-.708l-4-4a.5.5 0 0 0-.708 0l-4 4a.5.5 0 0 0 0 .708z"
+ },
"MEDIA.PREV": {
"section": "Media",
"title": "Previous",
diff --git a/ivette/src/dome/renderer/text/editors.tsx b/ivette/src/dome/renderer/text/editors.tsx
index e94492b865230fbb10e1520557f884015d0f662d..b0fe6f55e6fee056b640935f7e6f04e8f111f47a 100644
--- a/ivette/src/dome/renderer/text/editors.tsx
+++ b/ivette/src/dome/renderer/text/editors.tsx
@@ -40,6 +40,10 @@ 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';
diff --git a/ivette/src/frama-c/kernel/ASTinfo.tsx b/ivette/src/frama-c/kernel/ASTinfo.tsx
index 8eeff601e8c0a51ecd5b6460654bccddf4ce9e49..907787a07bc9b6d5ee54ea6b5263e640ff437866 100644
--- a/ivette/src/frama-c/kernel/ASTinfo.tsx
+++ b/ivette/src/frama-c/kernel/ASTinfo.tsx
@@ -362,7 +362,7 @@ export default function ASTinfo(): JSX.Element {
/>
</TitleBar>
<Boxes.Scroll>
- {markers.getSelected().map(renderMark)}
+ {React.Children.toArray(markers.getSelected().map(renderMark))}
</Boxes.Scroll>
</>
);
diff --git a/ivette/src/frama-c/kernel/ASTview.tsx b/ivette/src/frama-c/kernel/ASTview.tsx
index c2f657e33a1df75a9bfdec9fb8784c17dbf9e58b..6b1dd2729ad37bfe83625c86348ccb366d53ca4f 100644
--- a/ivette/src/frama-c/kernel/ASTview.tsx
+++ b/ivette/src/frama-c/kernel/ASTview.tsx
@@ -26,12 +26,16 @@
import React from 'react';
import _ from 'lodash';
+import CodeMirror from 'codemirror/lib/codemirror';
import * as Dome from 'dome';
import * as Settings from 'dome/data/settings';
+import { TitleBar } from 'ivette';
+import { IconButton } from 'dome/controls/buttons';
import type { key } from 'dome/data/json';
import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
+import { Filler, Inset } from 'dome/frame/toolbars';
import * as Preferences from 'ivette/prefs';
@@ -152,10 +156,10 @@ function getBulletColor(status: States.Tag): string {
function makeBullet(status: States.Tag): HTMLDivElement {
const marker = document.createElement('div');
marker.style.color = getBulletColor(status);
+ marker.style.textAlign = 'center';
if (status.descr)
marker.title = status.descr;
marker.innerHTML = 'â—‰';
- marker.align = 'center';
return marker;
}
@@ -182,25 +186,19 @@ export default function ASTview(): JSX.Element {
const statusDict = States.useTags(Properties.propStatusTags);
const setBullets = React.useCallback(() => {
- if (theFunction) {
- propertyStatus.forEach((prop) => {
- if (prop.fct === theFunction) {
- const status = statusDict.get(prop.status);
- if (status) {
- const bullet = makeBullet(status);
- const markers = buffer.findTextMarker(prop.key);
- markers.forEach((marker) => {
- const pos = marker.find();
- if (pos) {
- buffer.forEach((cm) => {
- cm.setGutterMarker(pos.from.line, 'bullet', bullet);
- });
- }
- });
- }
- }
- });
- }
+ propertyStatus.forEach((prop) => {
+ const status = statusDict.get(prop.status);
+ if (theFunction && prop.fct === theFunction && status) {
+ const bullet = makeBullet(status);
+ const markers = buffer.findTextMarker(prop.key);
+ buffer.forEach((cm) => {
+ markers.forEach((marker) => {
+ const line = marker.find()?.from.line;
+ if (line) cm.setGutterMarker(line, 'bullet', bullet);
+ });
+ });
+ }
+ });
}, [buffer, theFunction, propertyStatus, statusDict]);
React.useEffect(() => {
@@ -208,19 +206,19 @@ export default function ASTview(): JSX.Element {
return () => { buffer.off('change', setBullets); };
}, [buffer, setBullets]);
- async function reload(): Promise<void> {
+ const reload = React.useCallback(async () => {
printed.current = theFunction;
loadAST(buffer, theFunction, theMarker);
- }
+ }, [buffer, theFunction, theMarker]);
// Hook: async loading
- React.useEffect(() => {
- if (printed.current !== theFunction)
- reload();
- });
+ React.useEffect(() => { if (printed.current !== theFunction) reload(); });
// Also reload the buffer when the AST is recomputed.
- Server.onSignal(Ast.changed, reload);
+ React.useEffect(() => {
+ Server.onSignal(Ast.changed, reload);
+ return () => { Server.offSignal(Ast.changed, reload); };
+ });
React.useEffect(() => {
const decorator = (marker: string): string | undefined => {
@@ -313,9 +311,48 @@ export default function ASTview(): JSX.Element {
Dome.popupMenu(items);
}
+ const foldAll = (): void => buffer.forEach(CodeMirror.commands.foldAll);
+ const unfoldAll = (): void => buffer.forEach(CodeMirror.commands.unfoldAll);
+
+ const defaultFold = React.useCallback((): void => {
+ buffer.forEach((cm) => { CodeMirror.commands.unfoldAll(cm); });
+ }, [buffer]);
+
+ React.useEffect(() => {
+ buffer.on('change', defaultFold);
+ return () => { buffer.off('change', defaultFold); };
+ });
+
+ const foldOptions: CodeMirror.FoldOptions = {
+ rangeFinder: (cm, pos) => {
+ const range = CodeMirror.fold.comment(cm, pos);
+ /* Allows folding multi-line comments only. */
+ if (!range || range.from.line === range.to.line) return undefined;
+ return range;
+ }
+ };
+
// Component
return (
<>
+ <TitleBar>
+ <Filler />
+ <IconButton
+ icon='CHEVRON.CONTRACT'
+ visible={true}
+ onClick={foldAll}
+ title='Collapse all multi-line ACSL properties'
+ className="titlebar-thin-icon"
+ />
+ <IconButton
+ icon='CHEVRON.EXPAND'
+ visible={true}
+ onClick={unfoldAll}
+ title='Expand all multi-line ACSL properties'
+ className="titlebar-thin-icon"
+ />
+ <Inset />
+ </TitleBar>
<Text
buffer={buffer}
mode="text/x-csrc"
@@ -324,7 +361,9 @@ export default function ASTview(): JSX.Element {
onHover={onHover}
onSelection={onSelection}
onContextMenu={onContextMenu}
- gutters={['bullet']}
+ foldGutter={true}
+ foldOptions={foldOptions}
+ gutters={['bullet', 'CodeMirror-foldgutter']}
readOnly
/>
</>
diff --git a/ivette/src/frama-c/kernel/style.css b/ivette/src/frama-c/kernel/style.css
index 9b5d8f34ae951f23a7dd5595cb6267ef8d63b870..2ef1b533826dc78c29cf4fc7b15034a6854b4dbf 100644
--- a/ivette/src/frama-c/kernel/style.css
+++ b/ivette/src/frama-c/kernel/style.css
@@ -47,6 +47,11 @@
background: var(--code-bullet);
}
+/* More contrasted color for thinner icons. */
+.titlebar-thin-icon {
+ fill: var(--text);
+}
+
/* -------------------------------------------------------------------------- */
/* --- Globals --- */
/* -------------------------------------------------------------------------- */
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 61134be680a1e7fbd1fb15fddabbc0d372a4a22e..9b0ee6e61e2565b834785548bda0bec8c4e89dd2 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -478,7 +478,8 @@ let () = Request.register ~package
try
if not libc then Kernel.PrintLibc.set true ;
let global = Kernel_function.get_global kf in
- let ast = Jbuffer.to_json Printer.pp_global global in
+ let pp_glb = Printer.(with_unfold_precond (fun _ -> true) pp_global) in
+ let ast = Jbuffer.to_json pp_glb global in
if not libc then Kernel.PrintLibc.set false ; ast
with err ->
if not libc then Kernel.PrintLibc.set false ; raise err