Description:
------------
An extra char is written using highlight_file.

Test script:
---------------
<?php echo highlight_file(__FILE__); ?>

or

<?php echo highlight_string(file_get_contents(__FILE__)); ?>

Expected result:
----------------
<code><span style="color: #000000">
<br /></span><span style="color: #007700">echo&nbsp;</span><span style="color: 
#0000BB">highlight_file</span><span style="color: #007700">(</span><span<br />
</span>: #0000BB">__FILE__</span><span style="color: #007700">);
</span>
</code>

Actual result:
--------------
<code><span style="color: #000000">
<br /></span><span style="color: #007700">echo&nbsp;</span><span style="color: 
#0000BB">highlight_file</span><span style="color: #007700">(</span><span<br />
</span>: #0000BB">__FILE__</span><span style="color: #007700">);
</span>
</code>1