From 6d54985ad677015638d63aa29c45cf54b9b71bdc Mon Sep 17 00:00:00 2001 From: Antoine Musso Date: Wed, 13 Feb 2013 21:15:37 +0100 Subject: [PATCH] (bug 26204) font-size is too small The Geshi rendered output has a font-size of 10px where we would expect 13px just like for 
.

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
---
 SyntaxHighlight_GeSHi.class.php | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/SyntaxHighlight_GeSHi.class.php b/SyntaxHighlight_GeSHi.class.php
index 632c85d8..c413f534 100644
--- a/SyntaxHighlight_GeSHi.class.php
+++ b/SyntaxHighlight_GeSHi.class.php
@@ -287,6 +287,19 @@ class SyntaxHighlight_GeSHi {
 	 * @return string
 	 */
 	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;
 		$css = array();
 		$css[] = '