From 43c8a0f485c22b9caef4e42c2a917b09c4d92824 Mon Sep 17 00:00:00 2001
From: BurningTreeC <hypnotizedkangaroo@gmail.com>
Date: Thu, 15 Nov 2018 17:50:23 +0100
Subject: [PATCH] Keyboard Widget: refresh keyInfoArray (#3541)

this makes a keyboard widget update its keyInfoArray if its key has the `((descriptor))` format and one of the platform-specific configuration tiddlers with that descriptor-suffix changes
---
 core/modules/widgets/keyboard.js | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/core/modules/widgets/keyboard.js b/core/modules/widgets/keyboard.js
index f253d864a..9725bc0ab 100644
--- a/core/modules/widgets/keyboard.js
+++ b/core/modules/widgets/keyboard.js
@@ -79,6 +79,13 @@ KeyboardWidget.prototype.execute = function() {
 	this.tag = this.getAttribute("tag");
 	this.keyInfoArray = $tw.keyboardManager.parseKeyDescriptors(this.key);
 	this["class"] = this.getAttribute("class");
+	if(this.key.substr(0,2) === "((" && this.key.substr(-2,2) === "))") {
+		this.shortcutTiddlers = [];
+		var name = this.key.substring(2,this.key.length -2);
+		$tw.utils.each($tw.keyboardManager.lookupNames,function(platformDescriptor) {
+			self.shortcutTiddlers.push("$:/config/" + platformDescriptor + "/" + name);
+		});
+	}
 	// Make child widgets
 	this.makeChildWidgets();
 };
@@ -92,6 +99,10 @@ KeyboardWidget.prototype.refresh = function(changedTiddlers) {
 		this.refreshSelf();
 		return true;
 	}
+	// Update the keyInfoArray if one of its shortcut-config-tiddlers has changed
+	if(this.shortcutTiddlers && $tw.utils.hopArray(changedTiddlers,this.shortcutTiddlers)) {
+		this.keyInfoArray = $tw.keyboardManager.parseKeyDescriptors(this.key);
+	}
 	return this.refreshChildren(changedTiddlers);
 };