Add a font selector to the main page demo REPL

1 files changed, 10 insertions, 0 deletions

diff --git a/docs/repl.js b/docs/repl.js
index ecfed46e..3c744d23 100644
--- a/docs/repl.js
+++ b/docs/repl.js
@@ -107,6 +107,16 @@ doc.kb.onmousedown = ev => {
   }
 }
 
+if (doc.demo) {
+  let fonts=[["DejaVu","Mod"],["BQN386"],["Fairfax","HD"],["Julia","Mono"]];
+  let fontsel = '<select>'+fonts.map(f =>
+      '<option value="'+f[0]+'">'+f[0]+(f[1]?' '+f[1]:'')+'</option>'
+    ).join("")+'select';
+  doc.kb.innerHTML += fontsel;
+  doc.kb.querySelector('select').onchange =
+    e=>doc.cont.className='cont '+e.target.value;
+}
+
 if (doc.perm) doc.perm.onmouseover = doc.perm.onfocus = () => {
   let b=(new TextEncoder()).encode(doc.code.value);
   doc.perm.href='#code='+btoa(String.fromCharCode(...b));