ui.tools.listener-docs: add TIP: about the Ctrl-Break feature

char-rename
Alexander Iljin 2016-06-21 02:23:34 +03:00 committed by John Benediktsson
parent 2e49ffe6bd
commit 17aa171ccf
1 changed files with 6 additions and 4 deletions

View File

@ -1,7 +1,7 @@
USING: help.markup help.syntax help.tips io kernel listener sequences USING: help.markup help.syntax help.tips io kernel listener
ui.commands ui.gadgets.editors ui.gadgets.panes ui.operations sequences system ui.commands ui.gadgets.editors ui.gadgets.panes
ui.tools.common ui.tools.listener.completion vocabs vocabs.refresh ui.operations ui.tools.common ui.tools.listener.completion
words ; vocabs vocabs.refresh words ;
IN: ui.tools.listener IN: ui.tools.listener
HELP: <listener-gadget> HELP: <listener-gadget>
@ -97,4 +97,6 @@ TIP: "Scroll the listener from the keyboard by pressing " { $command listener-ga
TIP: "Press " { $command tool "common" refresh-all } " or run " { $link refresh-all } " to reload changed source files from disk." ; TIP: "Press " { $command tool "common" refresh-all } " or run " { $link refresh-all } " to reload changed source files from disk." ;
TIP: "On Windows: use C+Break to interrupt tight loops in your code started in the listener, such as" { $code "[ t ] [ ] while" } "Caution: this may crash the Factor runtime if the code uses cooperative multitasking or asynchronous I/O." ;
ABOUT: "ui-listener" ABOUT: "ui-listener"