src/Tools/jEdit/patches/extended_styles
changeset 72247 c06260b7152c
parent 71932 65fd0f032a75
child 73653 d9823224fcfe
--- a/src/Tools/jEdit/patches/extended_styles	Tue Sep 08 15:30:37 2020 +0100
+++ b/src/Tools/jEdit/patches/extended_styles	Tue Sep 08 21:14:42 2020 +0200
@@ -1,6 +1,6 @@
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2020-06-09 17:01:03.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2020-06-10 15:38:59.771992636 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-08 20:13:23.565140195 +0200
 @@ -332,9 +332,9 @@
  	//{{{ Package private members
  
@@ -13,7 +13,8 @@
  	//}}}
  
  	//{{{ Chunk constructor
-@@ -585,7 +585,7 @@
+@@ -584,8 +584,8 @@
+ 	// this is either style.getBackgroundColor() or
  	// styles[defaultID].getBackgroundColor()
  	private Color background;
 -	private char[] chars;
@@ -23,9 +24,9 @@
  	private GlyphData glyphData;
  	//}}}
  
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2020-05-20 11:10:10.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2020-06-10 15:38:03.605353644 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-03 05:31:01.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-08 20:13:23.569140077 +0200
 @@ -914,6 +914,11 @@
  		return chunkCache.getLineInfo(screenLine).physicalLine;
  	} //}}}
@@ -38,9 +39,9 @@
  	//{{{ getScreenLineOfOffset() method
  	/**
  	 * Returns the screen (wrapped) line containing the specified offset.
-diff -ru 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
---- 5.6pre1/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2020-05-20 11:10:13.000000000 +0200
-+++ 5.6pre1/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2020-06-10 16:10:50.165837982 +0200
+diff -ru 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+--- 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2020-09-03 05:31:09.000000000 +0200
++++ 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2020-09-08 20:13:23.569140077 +0200
 @@ -344,8 +344,28 @@
  			}
  		}