ui.tools.listener: add 'Help' button, and print message when listener exits, to reduce confusion if user presses C+d
parent
7e4b9b6377
commit
64a7fd0a4d
|
@ -386,6 +386,8 @@ interactor "completion" f {
|
||||||
error-summary? off
|
error-summary? off
|
||||||
tip-of-the-day. nl
|
tip-of-the-day. nl
|
||||||
listener
|
listener
|
||||||
|
nl
|
||||||
|
"The listener has exited. To start it again, click “Restart Listener”." print
|
||||||
] with-streams* ;
|
] with-streams* ;
|
||||||
|
|
||||||
: start-listener-thread ( listener -- )
|
: start-listener-thread ( listener -- )
|
||||||
|
@ -406,25 +408,22 @@ interactor "completion" f {
|
||||||
[ wait-for-listener ]
|
[ wait-for-listener ]
|
||||||
} cleave ;
|
} cleave ;
|
||||||
|
|
||||||
: listener-help ( -- ) "help.home" com-browse ;
|
: com-help ( -- ) "help.home" com-browse ;
|
||||||
|
|
||||||
\ listener-help H{ { +nullary+ t } } define-command
|
\ com-help H{ { +nullary+ t } } define-command
|
||||||
|
|
||||||
: com-auto-use ( -- )
|
: com-auto-use ( -- )
|
||||||
auto-use? [ not ] change ;
|
auto-use? [ not ] change ;
|
||||||
|
|
||||||
\ com-auto-use H{ { +nullary+ t } { +listener+ t } } define-command
|
\ com-auto-use H{ { +nullary+ t } { +listener+ t } } define-command
|
||||||
|
|
||||||
listener-gadget "misc" "Miscellaneous commands" {
|
|
||||||
{ T{ key-down f f "F1" } listener-help }
|
|
||||||
} define-command-map
|
|
||||||
|
|
||||||
listener-gadget "toolbar" f {
|
listener-gadget "toolbar" f {
|
||||||
{ f restart-listener }
|
{ f restart-listener }
|
||||||
{ T{ key-down f { A+ } "u" } com-auto-use }
|
{ T{ key-down f { A+ } "u" } com-auto-use }
|
||||||
{ T{ key-down f { A+ } "k" } clear-output }
|
{ T{ key-down f { A+ } "k" } clear-output }
|
||||||
{ T{ key-down f { A+ } "K" } clear-stack }
|
{ T{ key-down f { A+ } "K" } clear-stack }
|
||||||
{ T{ key-down f { C+ } "d" } com-end }
|
{ T{ key-down f { C+ } "d" } com-end }
|
||||||
|
{ T{ key-down f f "F1" } com-help }
|
||||||
} define-command-map
|
} define-command-map
|
||||||
|
|
||||||
listener-gadget "scrolling"
|
listener-gadget "scrolling"
|
||||||
|
|
Loading…
Reference in New Issue