wikimedia/mediawiki-extensions-SyntaxHighlight_GeSHi
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/SyntaxHighlight_GeSHi synced 2024-11-15 10:39:53 +00:00
Code Issues Packages Projects Releases Wiki Activity

(bug 26204) font-size is too small

Browse source 
The Geshi rendered output has a font-size of 10px where we would expect
13px just like for <pre>.

Bug 33496 against MediaWiki core dealt with that issue already: in some
(all?) browser 'monospace' has a size of 13px where as the default is
16px. When defining a font-size of 0.8em the monospace is scaled down to
10 px which is too small. By appending another font statement, the
browser treat monospace as a default font and thus scale it starting
with 16px instead of 13px.

This patch append a style to geshi which set the font-family to
"monospace, monospace" thus tricking the browser in considering
monospace a regular font.

Change-Id: I7bbdcc0a21010513473a7ca9d784df77e9920b5b
This commit is contained in:
Antoine Musso 2013-02-13 21:15:37 +01:00
parent f583c1186d
commit 6d54985ad6
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
SyntaxHighlight_GeSHi.class.php
View file

@ -287,6 +287,19 @@ class SyntaxHighlight_GeSHi {
* @return string * @return string
*/ */
public static function buildHeadItem( $geshi ) { public static function buildHeadItem( $geshi ) {
/**
* Geshi comes by default with a font-family set to monospace which
* ends ultimately ends up causing the font-size to be smaller than
* one would expect (causing bug 26204).
* We append to the default geshi style a CSS hack which is to specify
* monospace twice which "reset" the browser font-size specified for monospace.
*
* The hack is documented in MediaWiki core under
* docs/uidesign/monospace.html and in bug 33496.
*/
$geshi->set_code_style( 'font-family: monospace, monospace;',
/** preserve defaults */ true );
$lang = $geshi->language; $lang = $geshi->language;
$css = array(); $css = array();
$css[] = '<style type="text/css">/*<![CDATA[*/'; $css[] = '<style type="text/css">/*<![CDATA[*/';