Ensure that 'print_formatted_text' plays nice with patch_stdout.

Before this patch, `patch_stdout` was ignored completely.
Now, `print_formatted_text` does not require `patch_stdout`, it always print
above the prompt. For normal `print` statements, `patch_stdout` is still
required.