webstead: slightly more robust invocation of bedstead

Now we don't assume that stdout is line-buffered and that we'll
therefore get a single call to print().  Instead, we collect up all
the output in a string and use it when the program exits.

diff --git a/webstead.xhtml b/webstead.xhtml
index 3b582e4881ee06c530a4e33e12c4557e9aa418c7..0515640e9d16b201cba1037f45fe45939cea3a5d 100644 (file)
--- a/webstead.xhtml
+++ b/webstead.xhtml
@@ -75,18 +75,19 @@
         }
         if (c_update_needed)
             document.getElementById("c").value = ` {"${cstr}", U() },`;
+        var charstring = "";
         Bedstead({
-            arguments: args,
-            print: function(charstring) {
-                document.getElementById("rendered")
-                    .setAttribute("d", charstring
-                                  .replaceAll(/<!--(?:[^-]|-[^-])*-->/g, "")
-                                  .replace(/^.* [hv]stem /, "")
-                                  .replace(/^cntrmask [01]* /, "")
-                                  .replaceAll(/(\S+ +\S+ +)rmoveto/g, "m$1")
-                                  .replaceAll(/ rlineto/g, "")
-                                  .replace(/ endchar/, ""));
-            }
+            arguments: args,            
+            print: printed => charstring += printed
+        }).then(() => {
+            document.getElementById("rendered")
+                .setAttribute("d", charstring
+                              .replaceAll(/<!--(?:[^-]|-[^-])*-->/g, "")
+                              .replace(/^.* [hv]stem /, "")
+                              .replace(/^cntrmask [01]* /, "")
+                              .replaceAll(/(\S+ +\S+ +)rmoveto/g, "m$1")
+                              .replaceAll(/ rlineto/g, "")
+                              .replace(/ endchar/, ""));
         });
     }
     function from_c(c) {