src/Tools/jEdit/patches/extended_styles
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (3 months ago ago)
changeset 70019 4419d4d675c3
parent 67993 752a4e6d760c
permissions -rw-r--r--
formal update of patches -- no change of content;
wenzelm@67993
     1
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
wenzelm@67993
     2
--- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2018-04-09 01:57:24.000000000 +0200
wenzelm@70019
     3
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2019-02-24 12:32:09.336643045 +0100
wenzelm@67993
     4
@@ -322,9 +322,9 @@
wenzelm@50306
     5
 	//{{{ Package private members
wenzelm@50306
     6
 
wenzelm@50306
     7
 	//{{{ Instance variables
wenzelm@50306
     8
-	SyntaxStyle style;
wenzelm@50306
     9
+	public SyntaxStyle style;
wenzelm@50306
    10
 	// set up after init()
wenzelm@50306
    11
-	float width;
wenzelm@50306
    12
+	public float width;
wenzelm@50306
    13
 	//}}}
wenzelm@50306
    14
 
wenzelm@50306
    15
 	//{{{ Chunk constructor
wenzelm@67993
    16
@@ -572,7 +572,7 @@
wenzelm@48786
    17
 	// this is either style.getBackgroundColor() or
wenzelm@48786
    18
 	// styles[defaultID].getBackgroundColor()
wenzelm@48786
    19
 	private Color background;
wenzelm@48786
    20
-	private String str;
wenzelm@48786
    21
+	public String str;
wenzelm@50306
    22
 	private GlyphVector[] glyphs;
wenzelm@50306
    23
 	//}}}
wenzelm@50306
    24
 
wenzelm@67993
    25
diff -ru 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
wenzelm@67993
    26
--- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-09 01:58:01.000000000 +0200
wenzelm@70019
    27
+++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2019-02-24 12:20:10.550459878 +0100
wenzelm@65329
    28
@@ -917,6 +917,11 @@
wenzelm@61511
    29
 		return chunkCache.getLineInfo(screenLine).physicalLine;
wenzelm@61511
    30
 	} //}}}
wenzelm@61511
    31
 
wenzelm@61511
    32
+        public Chunk getChunksOfScreenLine(int screenLine)
wenzelm@61511
    33
+        {
wenzelm@61511
    34
+                return chunkCache.getLineInfo(screenLine).chunks;
wenzelm@61511
    35
+        }
wenzelm@61511
    36
+
wenzelm@61511
    37
 	//{{{ getScreenLineOfOffset() method
wenzelm@61511
    38
 	/**
wenzelm@61511
    39
 	 * Returns the screen (wrapped) line containing the specified offset.
wenzelm@67993
    40
diff -ru 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
wenzelm@67993
    41
--- 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2018-04-09 01:58:37.000000000 +0200
wenzelm@70019
    42
+++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2019-02-24 12:20:10.550459878 +0100
wenzelm@65329
    43
@@ -200,7 +200,24 @@
wenzelm@48786
    44
 	{
wenzelm@48786
    45
 		return loadStyles(family,size,true);
wenzelm@48786
    46
 	}
wenzelm@48786
    47
-	
wenzelm@48786
    48
+
wenzelm@48786
    49
+	/**
wenzelm@48786
    50
+	 * Extended styles derived from the user-specified style array.
wenzelm@48786
    51
+	 */
wenzelm@48786
    52
+
wenzelm@48786
    53
+	public static class StyleExtender
wenzelm@48786
    54
+	{
wenzelm@48786
    55
+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
wenzelm@48786
    56
+		{
wenzelm@48786
    57
+			return styles;
wenzelm@48786
    58
+		}
wenzelm@48786
    59
+	}
wenzelm@48786
    60
+	volatile private static StyleExtender _styleExtender = new StyleExtender();
wenzelm@48786
    61
+	public static void setStyleExtender(StyleExtender ext)
wenzelm@48786
    62
+	{
wenzelm@48786
    63
+		_styleExtender = ext;
wenzelm@48786
    64
+	}
wenzelm@48786
    65
+
wenzelm@48786
    66
 	/**
wenzelm@48786
    67
 	 * Loads the syntax styles from the properties, giving them the specified
wenzelm@48786
    68
 	 * base font family and size.
wenzelm@65329
    69
@@ -230,9 +247,11 @@
wenzelm@48786
    70
 				Log.log(Log.ERROR,StandardUtilities.class,e);
wenzelm@48786
    71
 			}
wenzelm@48786
    72
 		}
wenzelm@48786
    73
-
wenzelm@48786
    74
-		return styles;
wenzelm@61746
    75
+		styles[0] =
wenzelm@61746
    76
+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
wenzelm@61746
    77
+				null, new Font(family, 0, size));
wenzelm@48786
    78
+		return _styleExtender.extendStyles(styles);
wenzelm@48786
    79
 	} //}}}
wenzelm@48786
    80
-	
wenzelm@48786
    81
+
wenzelm@48786
    82
 	private SyntaxUtilities(){}
wenzelm@48786
    83
 }