From 4132767267da5b3bbf693b7f4b0e22e9b3b4ef25 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Fri, 29 Apr 2022 14:06:59 +0200
Subject: [PATCH] [ivette] Specifications folding
It uses the builtin feature of CodeMirror to do so.
There is several axes of improvement, but for now it should be enough.
---
ivette/src/dome/renderer/text/editors.tsx | 4 +
ivette/src/frama-c/kernel/ASTinfo.tsx | 2 +-
ivette/src/frama-c/kernel/ASTview.tsx | 96 ++++++++++++++++-------
src/plugins/server/kernel_ast.ml | 3 +-
4 files changed, 75 insertions(+), 30 deletions(-)
diff --git a/ivette/src/dome/renderer/text/editors.tsx b/ivette/src/dome/renderer/text/editors.tsx
index e94492b8652..b0fe6f55e6f 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 8eeff601e8c..907787a07bc 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 c2f657e33a1..46085ef7d6b 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 { Hfill } from 'dome/layout/boxes';
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,49 @@ 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.foldAll(cm);
+ cm.foldCode(0, undefined, 'unfold');
+ });
+ }, [buffer]);
+
+ React.useEffect(() => {
+ buffer.on('change', defaultFold);
+ return () => { buffer.off('change', defaultFold); };
+ });
+
+ const foldOptions: CodeMirror.FoldOptions = {
+ rangeFinder: (cm, pos) => {
+ const range = CodeMirror.fold.auto(cm, pos);
+ if (!range) return undefined;
+ const text = cm.getRange(range.from, range.to);
+ if (text.includes('sequence')) return undefined;
+ return range;
+ }
+ };
+
// Component
return (
<>
+ <TitleBar>
+ <Hfill />
+ <IconButton
+ icon='ANGLE.RIGHT'
+ visible={true}
+ onClick={foldAll}
+ title='Fold every specifications'
+ />
+ <IconButton
+ icon='ANGLE.DOWN'
+ visible={true}
+ onClick={unfoldAll}
+ title='Unfold every specifications'
+ />
+ </TitleBar>
<Text
buffer={buffer}
mode="text/x-csrc"
@@ -324,7 +362,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/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 61134be680a..9b0ee6e61e2 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
--
GitLab