Commit 47259490 authored by Michele Alberti's avatar Michele Alberti
Browse files

[ivette] Add frama-c/utils file, and add first function for printing text with tags.

parent 35546e40
......@@ -79,5 +79,7 @@ module.exports = {
"no-console": ["error", { allow: ["warn", "error"] }],
// Disallow the use of var in favor of let and const
"no-var": "error",
// Do not favor default import
"import/prefer-default-export": "off",
}
};
......@@ -33,11 +33,6 @@ export interface MarkerProps extends CodeMirror.TextMarkerOptions {
className?: string;
}
/**
* Text with tags.
*/
export type TextWithTags = null | string | TextWithTags[]
export interface CSSMarker {
/** Hover class `'dome-xHover-nnn'` */
classNameId: string;
......@@ -645,37 +640,6 @@ export class RichTextBuffer extends Emitter {
}
}
// --------------------------------------------------------------------------
// --- Print Utilities
// --------------------------------------------------------------------------
/**
* Print text containing tags into buffer.
* @param options Specify particular marker options.
*/
printTextWithTags(contents: TextWithTags, options?: MarkerProps) {
if (Array.isArray(contents)) {
let marker = false;
const tag = contents.shift();
if (tag) {
if (Array.isArray(tag)) {
contents.unshift(tag);
} else {
this.openTextMarker({ id: tag, ...options ?? {} });
marker = true;
}
}
contents.forEach((txt) => this.printTextWithTags(txt, options ?? {}));
if (marker) {
marker = false;
this.closeTextMarker();
}
} else if (typeof contents === 'string') {
this.append(contents);
} else {
console.error('[Dome.buffers] Unexpected text', contents);
}
}
}
// --------------------------------------------------------------------------
// --------------------------------------------------------------------------
// --- Frama-C Utilities
// --------------------------------------------------------------------------
/**
* @packageDocumentation
* @module frama-c/utils
*/
import * as DomeBuffers from 'dome/text/buffers';
import * as KernelData from 'api/kernel/data';
// --------------------------------------------------------------------------
// --- Print Utilities
// --------------------------------------------------------------------------
/**
* Print text containing tags into buffer.
* @param options Specify particular marker options.
*/
export function printTextWithTags(
buffer: DomeBuffers.RichTextBuffer,
contents: KernelData.text,
options?: DomeBuffers.MarkerProps,
) {
if (Array.isArray(contents)) {
let marker = false;
const tag = contents.shift();
if (tag) {
if (Array.isArray(tag)) {
contents.unshift(tag);
} else {
buffer.openTextMarker({ id: tag, ...options ?? {} });
marker = true;
}
}
contents.forEach((txt) => printTextWithTags(buffer, txt, options));
if (marker) {
marker = false;
buffer.closeTextMarker();
}
} else if (typeof contents === 'string') {
buffer.append(contents);
} else {
console.error('[Dome.buffers] Unexpected text', contents);
}
}
......@@ -4,6 +4,7 @@
import React from 'react';
import * as States from 'frama-c/states';
import * as Utils from 'frama-c/utils';
import { Vfill } from 'dome/layout/boxes';
import { RichTextBuffer } from 'dome/text/buffers';
......@@ -26,7 +27,7 @@ const ASTinfo = () => {
React.useEffect(() => {
buffer.clear();
if (data) {
buffer.printTextWithTags(data, { css: 'color: blue' });
Utils.printTextWithTags(buffer, data, { css: 'color: blue' });
}
}, [buffer, data]);
......
......@@ -6,6 +6,7 @@ import React from 'react';
import _ from 'lodash';
import * as Server from 'frama-c/server';
import * as States from 'frama-c/states';
import * as Utils from 'frama-c/utils';
import * as Dome from 'dome';
import { RichTextBuffer } from 'dome/text/buffers';
......@@ -49,7 +50,7 @@ async function loadAST(
if (!data) {
buffer.log('// No code for function', theFunction);
}
buffer.printTextWithTags(data);
Utils.printTextWithTags(buffer, data);
if (theMarker)
buffer.scroll(theMarker);
} catch (err) {
......
Markdown is supported
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