author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 65329 | 4f3da52cec02 |
child 67992 | 752a4e6d760c |
permissions | -rw-r--r-- |
65329 | 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 |
2 |
--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2017-03-18 14:30:28.000000000 +0100 |
|
3 |
+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2017-03-19 19:27:45.730945687 +0100 |
|
59571 | 4 |
@@ -259,9 +259,9 @@ |
50306 | 5 |
//{{{ Package private members |
6 |
||
7 |
//{{{ Instance variables |
|
8 |
- SyntaxStyle style; |
|
9 |
+ public SyntaxStyle style; |
|
10 |
// set up after init() |
|
11 |
- float width; |
|
12 |
+ public float width; |
|
13 |
//}}} |
|
14 |
||
15 |
//{{{ Chunk constructor |
|
59571 | 16 |
@@ -509,7 +509,7 @@ |
48786 | 17 |
// this is either style.getBackgroundColor() or |
18 |
// styles[defaultID].getBackgroundColor() |
|
19 |
private Color background; |
|
20 |
- private String str; |
|
21 |
+ public String str; |
|
50306 | 22 |
private GlyphVector[] glyphs; |
23 |
//}}} |
|
24 |
||
65329 | 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 |
26 |
--- 5.4.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2017-03-18 14:30:28.000000000 +0100 |
|
27 |
+++ 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2017-03-19 19:27:45.734945702 +0100 |
|
28 |
@@ -917,6 +917,11 @@ |
|
61511 | 29 |
return chunkCache.getLineInfo(screenLine).physicalLine; |
30 |
} //}}} |
|
31 |
||
32 |
+ public Chunk getChunksOfScreenLine(int screenLine) |
|
33 |
+ { |
|
34 |
+ return chunkCache.getLineInfo(screenLine).chunks; |
|
35 |
+ } |
|
36 |
+ |
|
37 |
//{{{ getScreenLineOfOffset() method |
|
38 |
/** |
|
39 |
* Returns the screen (wrapped) line containing the specified offset. |
|
65329 | 40 |
Only in 5.4.0/jEdit-patched/org/gjt/sp/jedit/textarea: TextArea.java.orig |
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 |
|
42 |
--- 5.4.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2017-03-18 14:30:34.000000000 +0100 |
|
43 |
+++ 5.4.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2017-03-19 19:27:45.734945702 +0100 |
|
44 |
@@ -200,7 +200,24 @@ |
|
48786 | 45 |
{ |
46 |
return loadStyles(family,size,true); |
|
47 |
} |
|
48 |
- |
|
49 |
+ |
|
50 |
+ /** |
|
51 |
+ * Extended styles derived from the user-specified style array. |
|
52 |
+ */ |
|
53 |
+ |
|
54 |
+ public static class StyleExtender |
|
55 |
+ { |
|
56 |
+ public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) |
|
57 |
+ { |
|
58 |
+ return styles; |
|
59 |
+ } |
|
60 |
+ } |
|
61 |
+ volatile private static StyleExtender _styleExtender = new StyleExtender(); |
|
62 |
+ public static void setStyleExtender(StyleExtender ext) |
|
63 |
+ { |
|
64 |
+ _styleExtender = ext; |
|
65 |
+ } |
|
66 |
+ |
|
67 |
/** |
|
68 |
* Loads the syntax styles from the properties, giving them the specified |
|
69 |
* base font family and size. |
|
65329 | 70 |
@@ -230,9 +247,11 @@ |
48786 | 71 |
Log.log(Log.ERROR,StandardUtilities.class,e); |
72 |
} |
|
73 |
} |
|
74 |
- |
|
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 | 79 |
+ return _styleExtender.extendStyles(styles); |
80 |
} //}}} |
|
81 |
- |
|
82 |
+ |
|
83 |
private SyntaxUtilities(){} |
|
84 |
} |