From 89faff96938d771b9a28e0fc4d2fb188eca4d85a Mon Sep 17 00:00:00 2001 From: jmoenig Date: Thu, 28 May 2020 12:45:05 +0200 Subject: [PATCH] replaced unicode in microphone menu with new drawn symbols --- src/gui.js | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/src/gui.js b/src/gui.js index 30ba957b..5dfc504b 100644 --- a/src/gui.js +++ b/src/gui.js @@ -5369,19 +5369,34 @@ IDE_Morph.prototype.microphoneMenu = function () { world = this.world(), pos = this.controlBar.settingsButton.bottomLeft(), resolutions = ['low', 'normal', 'high', 'max'], - microphone = this.stage.microphone; + microphone = this.stage.microphone, + tick = new SymbolMorph( + 'tick', + MorphicPreferences.menuFontSize * 0.75 + ), + on = new SymbolMorph( + 'checkedBox', + MorphicPreferences.menuFontSize * 0.75 + ), + empty = tick.fullCopy(); + empty.render = nop; if (microphone.isReady) { menu.addItem( - '\u2611 ' + localize('Microphone'), + [ + on, + localize('Microphone') + ], () => microphone.stop() ); menu.addLine(); } resolutions.forEach((res, i) => { menu.addItem( - (microphone.resolution === i + 1 ? '\u2713 ' : ' ') + - localize(res), + [ + microphone.resolution === i + 1 ? tick : empty, + localize(res) + ], () => microphone.setResolution(i + 1) ); });