+: help-script ( -- xml )
+ [XML
+ <script type="text/javascript">
+ document.addEventListener('keydown', function (event) {
+ if (event.code == 'Slash') {
+ let input = document.getElementById('search');
+ if (input !== document.activeElement) {
+ setTimeout(function() {
+ input.focus().select()
+ }, 0);
+ }
+ }
+ });
+ </script>
+ XML] ;
+
+: help-header ( stylesheet -- xml )
+ help-stylesheet help-meta swap help-script 3append ;
+