From 5b712898ece65a1a5a565606813ac4b35387638d Mon Sep 17 00:00:00 2001
From: Marshall Lochbaum <mwlochbaum@gmail.com>
Date: Sat, 21 Nov 2020 20:51:34 -0500
Subject: Add a font selector to the main page demo REPL

---
 docs/repl.js | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'docs/repl.js')

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));
-- 
cgit v1.2.3