diff --git a/ui-js/coq-manager.js b/ui-js/coq-manager.js
index 4c88927db784bf9590cff25daffe40888aa55afa..527d812a5cb84d2bc8bc6f1c72540cd0136435c2 100644
--- a/ui-js/coq-manager.js
+++ b/ui-js/coq-manager.js
@@ -595,7 +595,7 @@ class CoqManager {
 
     feedMessage(sid, lvl, loc, msg) {
 
-        var fmsg = this.pprint.pp2DOM(msg);
+        var fmsg = this.pprint.msg2DOM(msg);
 
         lvl = lvl[0];  // JSON encoding
 
@@ -717,7 +717,7 @@ class CoqManager {
 
     coqLog(level, msg) {
 
-        let fmsg = this.pprint.pp2DOM(msg);
+        let fmsg = this.pprint.msg2DOM(msg);
 
         level = level[0];
 
@@ -743,7 +743,7 @@ class CoqManager {
         if (this.error.some(stm => stm.feedback.some(x => arreq_deep(x.msg, msg))))
             return;
 
-        var fmsg = this.pprint.pp2DOM(msg);
+        var fmsg = this.pprint.msg2DOM(msg);
 
         var item = this.layout.log(fmsg, 'Error', sids && {'data-coq-sid': sids[0]});
         this.pprint.adjustBreaks(item);
@@ -1473,7 +1473,7 @@ class CoqContextualInfo {
     }
 
     formatMessages(msgs) {
-        var ppmsgs = msgs.map(feedback => this.pprint.pp2DOM(feedback.msg)),
+        var ppmsgs = msgs.map(feedback => this.pprint.msg2DOM(feedback.msg)),
             frag = $(document.createDocumentFragment());
 
         for (let e of ppmsgs) {
diff --git a/ui-js/format-pprint.js b/ui-js/format-pprint.js
index 75634c3d3f3e894550c4f389b363de0500fa2639..db40ef5f9c126c2832e1554030e3d580b4dcf52a 100644
--- a/ui-js/format-pprint.js
+++ b/ui-js/format-pprint.js
@@ -41,12 +41,19 @@ class FormatPrettyPrint {
     /**
      * Formats a pretty-printed element to be displayed in an HTML document.
      * @param {array} pp a serialized Pp element
+     * @param {topBox} string wrap with a box ('vertical' / 'horizontal')
      */
-    pp2DOM(pp) {
-        if (pp.constructor !== Array) {
+    pp2DOM(pp, topBox) {
+        if (!Array.isArray(pp)) {
             throw new Error("malformed Pp element: " + pp);
         }
 
+        if (topBox) {
+            var dom = this.pp2DOM(pp);
+            return (dom.length == 1 && dom.is('.Pp_box')) ? dom :
+                this.makeBox(dom, topBox);
+        }
+
         var [tag, ct] = pp;
 
         switch (tag) {
@@ -62,9 +69,7 @@ class FormatPrettyPrint {
         // ["Pp_box", ["Pp_vbox"/"Pp_hvbox"/"Pp_hovbox", _], content]
         case "Pp_box":
             let mode = ct[0] == 'Pp_vbox' ? 'vertical' : 'horizontal';
-            return this.adjustBox(
-                $('<div>').addClass('Pp_box').attr('data-mode', mode)
-                    .append(this.pp2DOM(pp[2])));
+            return this.makeBox(this.pp2DOM(pp[2]), mode);
 
         // ["Pp_tag", tag, content]
         case "Pp_tag":
@@ -267,6 +272,10 @@ class FormatPrettyPrint {
         return ret;
     }
 
+    msg2DOM(msg) {
+        return this.pp2DOM(msg, 'horizontal');
+    }
+
     /**
      * Formats the current proof state.
      * @param {object} goals a record of proof goals 
@@ -333,7 +342,7 @@ class FormatPrettyPrint {
             $('<div>').addClass(['coq-hypothesis', h_def && 'coq-has-def'])
                 .append(h_names.map(mklabel))
                 .append(h_def && mkdef(h_def))
-                .append(this.pp2DOM(h_type)));
+                .append($('<div>').append(this.pp2DOM(h_type))));
         let ty = this.pp2DOM(goal.ty);
         return $('<div>').addClass('coq-env').append(hyps, $('<hr/>'), ty);
     }
@@ -349,6 +358,12 @@ class FormatPrettyPrint {
             : 1;
     }
 
+    makeBox(jdom, mode) {
+        return this.adjustBox(
+            $('<div>').addClass('Pp_box').attr('data-mode', mode)
+                .append(jdom));
+    }
+
     adjustBox(jdom) {
         let mode = jdom.attr('data-mode');
 
@@ -368,7 +383,7 @@ class FormatPrettyPrint {
      */
     adjustBreaks(jdom) {
         var width = jdom.width(),
-            boxes = jdom.add(jdom.find('.Pp_box'));
+            boxes = jdom.find('.Pp_box');
 
         var indent = 0;
         function breakAt(brk) {
@@ -379,7 +394,7 @@ class FormatPrettyPrint {
 
         for (let el of boxes) {
             let box = $(el),
-                mode = box.attr('data-mode'),
+                mode = box.attr('data-mode') || 'horizontal',
                 brks = box.children('.Pp_break');
             if (mode == 'horizontal') {
                 var prev = null;
@@ -399,10 +414,14 @@ class FormatPrettyPrint {
             }
         }
 
-        if (jdom.children().length == 0)
+        if (this._isFlat(jdom))
             jdom.addClass("text-only");
     }
 
+    _isFlat(jdom) {
+        return jdom.find('.Pp_break').length == 0;
+    }
+
     /**
      * Auxiliary method that wraps a node with an element, but excludes
      * leading and trailing spaces. These are attached outside the wrapper.