src/Tools/jEdit/patches/extended_styles
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 65329 4f3da52cec02
child 67992 752a4e6d760c
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
     1
diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
     2
--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java	2017-03-18 14:30:28.000000000 +0100
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
     3
+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2017-03-19 19:27:45.730945687 +0100
59571
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 53898
diff changeset
     4
@@ -259,9 +259,9 @@
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
     5
 	//{{{ Package private members
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
     6
 
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
     7
 	//{{{ Instance variables
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
     8
-	SyntaxStyle style;
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
     9
+	public SyntaxStyle style;
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    10
 	// set up after init()
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    11
-	float width;
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    12
+	public float width;
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    13
 	//}}}
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    14
 
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    15
 	//{{{ Chunk constructor
59571
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 53898
diff changeset
    16
@@ -509,7 +509,7 @@
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    17
 	// this is either style.getBackgroundColor() or
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    18
 	// styles[defaultID].getBackgroundColor()
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    19
 	private Color background;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    20
-	private String str;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    21
+	public String str;
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    22
 	private GlyphVector[] glyphs;
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    23
 	//}}}
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    24
 
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    25
diff -ru 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    26
--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java	2017-03-18 14:30:28.000000000 +0100
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    27
+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2017-03-19 19:27:45.734945702 +0100
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    28
@@ -917,6 +917,11 @@
61511
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    29
 		return chunkCache.getLineInfo(screenLine).physicalLine;
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    30
 	} //}}}
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    31
 
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    32
+        public Chunk getChunksOfScreenLine(int screenLine)
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    33
+        {
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    34
+                return chunkCache.getLineInfo(screenLine).chunks;
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    35
+        }
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    36
+
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    37
 	//{{{ getScreenLineOfOffset() method
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    38
 	/**
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    39
 	 * Returns the screen (wrapped) line containing the specified offset.
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    40
Only in 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea: TextArea.java.orig
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    41
diff -ru 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    42
--- 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java	2017-03-18 14:30:34.000000000 +0100
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    43
+++ 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2017-03-19 19:27:45.734945702 +0100
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    44
@@ -200,7 +200,24 @@
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    45
 	{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    46
 		return loadStyles(family,size,true);
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    47
 	}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    48
-	
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    49
+
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    50
+	/**
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    51
+	 * Extended styles derived from the user-specified style array.
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    52
+	 */
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    53
+
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    54
+	public static class StyleExtender
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    55
+	{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    56
+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    57
+		{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    58
+			return styles;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    59
+		}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    60
+	}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    61
+	volatile private static StyleExtender _styleExtender = new StyleExtender();
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    62
+	public static void setStyleExtender(StyleExtender ext)
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    63
+	{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    64
+		_styleExtender = ext;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    65
+	}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    66
+
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    67
 	/**
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    68
 	 * Loads the syntax styles from the properties, giving them the specified
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    69
 	 * base font family and size.
65329
4f3da52cec02 updated to jedit-5.4.0;
wenzelm
parents: 61746
diff changeset
    70
@@ -230,9 +247,11 @@
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    71
 				Log.log(Log.ERROR,StandardUtilities.class,e);
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    72
 			}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    73
 		}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    74
-
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    75
-		return styles;
61746
3df1b6a5837c paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
wenzelm
parents: 61511
diff changeset
    76
+		styles[0] =
3df1b6a5837c paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
wenzelm
parents: 61511
diff changeset
    77
+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
3df1b6a5837c paint gutter text on base line of main text area, to accomodate extra line spacing without special tricks (see also jEdit bug #3717 and its fix in SVN 23977, which does not quite work: odd jumping positions on vertical cursor movement);
wenzelm
parents: 61511
diff changeset
    78
+				null, new Font(family, 0, size));
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    79
+		return _styleExtender.extendStyles(styles);
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    80
 	} //}}}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    81
-	
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    82
+
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    83
 	private SyntaxUtilities(){}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    84
 }