[ jEdit-commits ] SF.net SVN: jedit:[24465] plugins/Highlight/trunk

[<kp...@us...>]

Revision: 24465
          http://sourceforge.net/p/jedit/svn/24465
Author:   kpouer
Date:     2016-07-22 12:22:51 +0000 (Fri, 22 Jul 2016)
Log Message:
-----------
Allow negative line spacing (patch #171 from Makarius)

Modified Paths:
--------------
    plugins/Highlight/trunk/docs/Highlight.html
    plugins/Highlight/trunk/src/gatchan/highlight/Highlighter.java

Modified: plugins/Highlight/trunk/docs/Highlight.html
===================================================================
--- plugins/Highlight/trunk/docs/Highlight.html	2016-07-19 14:47:33 UTC (rev 24464)
+++ plugins/Highlight/trunk/docs/Highlight.html	2016-07-22 12:22:51 UTC (rev 24465)
@@ -42,8 +42,9 @@
 </p>
 <h2>History</h2>
 <ul>
-    <li>2.3 (Feb 15, 2016)</li>
+    <li>2.3 (Jul 22, 2016)</li>
     <ul>
+        <li>Allow negative line spacing (patch #171 from Makarius)</li>
         <li>Ok & Cancel buttons now use common labels (patch #174 from Makarius)</li>
         <li>Add an option to ignore selections smaller than a number of char</li>
         <li>Fix highlight selection under caret not working in splitted panes</li>

Modified: plugins/Highlight/trunk/src/gatchan/highlight/Highlighter.java
===================================================================
--- plugins/Highlight/trunk/src/gatchan/highlight/Highlighter.java	2016-07-19 14:47:33 UTC (rev 24464)
+++ plugins/Highlight/trunk/src/gatchan/highlight/Highlighter.java	2016-07-22 12:22:51 UTC (rev 24465)
@@ -272,8 +272,8 @@
 		if (filled)
 		{
 			int lineHeight = painter.getLineHeight();
-			int charHeight = painter.getFontHeight();
-			int charOffset = lineHeight - charHeight;
+			int charHeight = Math.min(lineHeight, painter.getFontHeight());
+			int charOffset = Math.max(lineHeight - charHeight, 0);
 			if (roundcorner)
 			{
 				gfx.fillRoundRect(startX, y + charOffset, endX - startX, charHeight - 1, 5, 5);
@@ -302,8 +302,8 @@
 	private void drawRect(Graphics2D gfx, int y, int startX, int endX)
 	{
 		int lineHeight = painter.getLineHeight();
-		int charHeight = painter.getFontHeight();
-		int charOffset = lineHeight - charHeight;
+		int charHeight = Math.min(lineHeight, painter.getFontHeight());
+		int charOffset = Math.max(lineHeight - charHeight, 0);
 		if (roundcorner)
 			gfx.drawRoundRect(startX, y + charOffset, endX - startX, charHeight - 1,5,5);
 		else

This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.