Reinstate the prettyPrint radio on the playground (#511)

Author: tmke8

playground/index.html

@@ -41,6 +41,30 @@ <h3>Math font:</h3>
                                 </select>
                             </div>
                         </div>
+                        <div id="prettyprint" class="option-group">
+                            <h3>Pretty print:</h3>
+                            <div class="options">
+                                <label
+                                    ><input
+                                        type="radio"
+                                        id="pretty-true"
+                                        name="prettyprint"
+                                        value="true"
+                                        checked
+                                    />
+                                    True</label
+                                >
+                                <label
+                                    ><input
+                                        type="radio"
+                                        id="pretty-false"
+                                        name="prettyprint"
+                                        value="false"
+                                    />
+                                    False</label
+                                >
+                            </div>
+                        </div>
                         <div id="displaystyle" class="option-group">
                             <h3>Display style:</h3>
                             <div class="options">
@@ -71,7 +95,6 @@ <h3>Display style:</h3>
                     <summary><strong>JSON config</strong> (click to open)</summary>
                     <div>
                         <textarea rows="10" id="configField" spellcheck="false">{
-    "prettyPrint": true,
     "macros": {
         "d": "\\mathrm{d}\\mspace{0mu}",
         "ceil": "\\lceil #1 \\rceil",

playground/main.js

@@ -19,18 +19,25 @@ function updateIsBlockCache() {
 }
 
 function updateConfig() {
+  const prettyRadio = document.querySelector(
+    '#prettyprint input[type="radio"]:checked',
+  );
+  const isPrettyPrint = prettyRadio ? prettyRadio.value === "true" : true;
+
   const configField = document.getElementById("configField");
 
   try {
     const jsonString = configField.value.trim();
 
     // Parse JSON with custom reviver to convert macros to Map
-    const parsed = JSON.parse(jsonString, (key, value) => {
+    let parsed = JSON.parse(jsonString, (key, value) => {
       if (key === 'macros') {
         return new Map(Object.entries(value));
       }
       return value;
     });
+    // Set the prettyPrint property from the radio selection
+    parsed["prettyPrint"] = isPrettyPrint;
     set_config(parsed);
 
   } catch (error) {
@@ -246,6 +253,15 @@ document.addEventListener("DOMContentLoaded", () => {
       });
     });
 
+  document
+    .querySelectorAll('#prettyprint input[type="radio"]')
+    .forEach((radio) => {
+      radio.addEventListener("change", () => {
+        updateConfig(); // Update config when radio button changes
+        updateOutput();
+      });
+    });
+
   // Add listener for config field changes
   configField.addEventListener("input", () => {
     const success = updateConfig(); // Update config when textarea content changes