<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Sounds great. As long as we have a nice fallback if pygment is not<br>

installed/non functional.<br>
</blockquote><div><br>I think the there are a couple of fallbacks:<br><br>* Just no coloring - everything works, but you get uncolored text.<br>* Any frontend can do its own coloring if it wants.<br><br>What I wouldn&#39;t want to do is still maintain our own coloring code because (in my mind) the goal of this transition is to get away from that.† If we really wanted to make sure that coloring always worked, we could just ship pygments in IPython.external<br>
†<br>Would this satisfy you?<br><br>Brian<br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>
GaŽl<br>
</blockquote></div><br>