From 8433cb6ac3369f03c4ed2d87411365d1f39d8ea0 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 2 Jun 2020 17:02:57 +0200
Subject: [PATCH] [Dome][Ivette] Add function to print text with tags, and use
 in Ivette components.

---
 ivette/src/dome/src/renderer/text/buffers.js | 31 ++++++++++++++++++++
 ivette/src/renderer/ASTinfo.tsx              | 17 +----------
 ivette/src/renderer/ASTview.tsx              | 20 ++-----------
 3 files changed, 35 insertions(+), 33 deletions(-)

diff --git a/ivette/src/dome/src/renderer/text/buffers.js b/ivette/src/dome/src/renderer/text/buffers.js
index 30c272d3f99..0c0265b7849 100644
--- a/ivette/src/dome/src/renderer/text/buffers.js
+++ b/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}'.`
+      );
+    }
+  }
+
 }
 
 // --------------------------------------------------------------------------
diff --git a/ivette/src/renderer/ASTinfo.tsx b/ivette/src/renderer/ASTinfo.tsx
index 1fe3f3eb8c4..e505f52dbcd 100644
--- a/ivette/src/renderer/ASTinfo.tsx
+++ b/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]);
 
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 80b33c5760b..3fc396103d7 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/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);
         });
-- 
GitLab