[Dome][Ivette] Add function to print text with tags, and use in Ivette components.

ivette/src/dome/src/renderer/text/buffers.js

@@ -540,6 +540,37 @@ is blocked.
       .finally(endOperation);
   }
 
+  // --------------------------------------------------------------------------
+  // --- Print Utilities
+  // --------------------------------------------------------------------------
+
+  /**
+     @summary Print text containing tags into buffer (bound to `this`).
+     @param {string|string[]} text - Text to print.
+     @param {object} options - CodeMirror
+       [text marker](https://codemirror.net/doc/manual.html#api_marker) options.
+  */
+  printTextWithTags(text, options = {}) {
+    if (Array.isArray(text)) {
+      const tag = text.shift();
+      if (tag !== '') {
+        const markerOptions = { id: tag, ...options };
+        this.openTextMarker(markerOptions);
+      }
+      text.forEach((txt) => this.printTextWithTags(txt, options));
+      if (tag !== '') {
+        this.closeTextMarker();
+      }
+    } else if (typeof (text) === 'string') {
+      this.append(text);
+    } else { // This case should be useless when using TS.
+      console.error(
+        `Function 'printTextWithTags' accepts a parameter of `
+        + `type string or string array: got '${typeof text}'.`
+      );
+    }
+  }
+
 }
 
 // --------------------------------------------------------------------------

ivette/src/renderer/ASTinfo.tsx

@@ -14,21 +14,6 @@ import { Component } from 'frama-c/LabViews';
 // --- Information Panel
 // --------------------------------------------------------------------------
 
-const printInfo = (buffer: RichTextBuffer, text: string | string[]) => {
-  if (Array.isArray(text)) {
-    const tag = text.shift();
-    if (tag !== '') {
-      buffer.openTextMarker({ id: tag, css: 'color: blue' });
-    }
-    text.forEach((txt) => printInfo(buffer, txt));
-    if (tag !== '') {
-      buffer.closeTextMarker();
-    }
-  } else {
-    buffer.append(text);
-  }
-};
-
 const ASTinfo = () => {
 
   const buffer = React.useMemo(() => new RichTextBuffer(), []);
@@ -39,7 +24,7 @@ const ASTinfo = () => {
   React.useEffect(() => {
     buffer.clear();
     if (data) {
-      printInfo(buffer, data);
+      buffer.printTextWithTags(data, { css: 'color: blue' });
     }
   }, [buffer, data]);
 

ivette/src/renderer/ASTview.tsx

@@ -33,21 +33,6 @@ const PP = new Dome.PP('AST View');
 // --- Rich Text Printer
 // --------------------------------------------------------------------------
 
-const printAST = (buffer: RichTextBuffer, text: string) => {
-  if (Array.isArray(text)) {
-    const tag = text.shift();
-    if (tag !== '') {
-      buffer.openTextMarker({ id: tag });
-    }
-    text.forEach((txt) => printAST(buffer, txt));
-    if (tag !== '') {
-      buffer.closeTextMarker();
-    }
-  } else if (typeof (text) === 'string') {
-    buffer.append(text);
-  }
-};
-
 async function loadAST(
   buffer: RichTextBuffer, theFunction?: string, theMarker?: string,
 ) {
@@ -62,9 +47,10 @@ async function loadAST(
         });
         buffer.operation(() => {
           buffer.clear();
-          if (!data)
+          if (!data) {
             buffer.log('// No code for function ', theFunction);
-          printAST(buffer, data);
+          }
+          buffer.printTextWithTags(data);
           if (theMarker)
             buffer.scroll(theMarker, undefined);
         });