| author | wenzelm | 
| Fri, 23 Aug 2024 15:44:31 +0200 | |
| changeset 80747 | af1b83f0dc5f | 
| parent 80156 | 70d69b081561 | 
| child 81297 | 07f64697408e | 
| permissions | -rw-r--r-- | 
| 73653 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 1 | diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java | 
| 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 2 | --- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200 | 
| 80156 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 3 | +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java 2024-04-25 12:56:22.208257322 +0200 | 
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 4 | @@ -332,9 +332,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
 | |
| 72247 | 16 | @@ -584,8 +584,8 @@ | 
| 17 | // this is either style.getBackgroundColor() or | |
| 48786 | 18 | // styles[defaultID].getBackgroundColor() | 
| 19 | private Color background; | |
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 20 | - private char[] chars; | 
| 48786 | 21 | - private String str; | 
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 22 | + public char[] chars; | 
| 48786 | 23 | + public String str; | 
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 24 | private GlyphData glyphData; | 
| 50306 | 25 | //}}} | 
| 26 | ||
| 80156 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 27 | @@ -926,6 +926,11 @@ | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 28 | } | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 29 | |
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 30 | @Override | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 31 | +		public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
 | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 32 | +			synchronized (this) { return super.computeIfAbsent(key, f); }
 | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 33 | + } | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 34 | + | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 35 | + @Override | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 36 | protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest) | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 37 |  		{
 | 
| 
70d69b081561
more robust: avoid spurious ConcurrentModificationException;
 wenzelm parents: 
79012diff
changeset | 38 | return size() > capacity; | 
| 73653 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 39 | diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java | 
| 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 40 | --- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200 | 
| 79012 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 41 | +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2023-11-20 15:31:55.825519645 +0100 | 
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 42 | @@ -914,6 +914,11 @@ | 
| 61511 | 43 | return chunkCache.getLineInfo(screenLine).physicalLine; | 
| 44 | } //}}} | |
| 45 | ||
| 46 | + public Chunk getChunksOfScreenLine(int screenLine) | |
| 47 | +        {
 | |
| 48 | + return chunkCache.getLineInfo(screenLine).chunks; | |
| 49 | + } | |
| 50 | + | |
| 51 |  	//{{{ getScreenLineOfOffset() method
 | |
| 52 | /** | |
| 53 | * Returns the screen (wrapped) line containing the specified offset. | |
| 73658 | 54 | @@ -1622,8 +1627,8 @@ | 
| 55 | } | |
| 56 | ||
| 57 | // Scan backwards, trying to find a bracket | |
| 58 | -		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
 | |
| 59 | - String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫"; | |
| 60 | +		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉";
 | |
| 61 | + String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊"; | |
| 62 | int count = 1; | |
| 63 | char openBracket = '\0'; | |
| 64 | char closeBracket = '\0'; | |
| 79012 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 65 | @@ -6336,7 +6341,7 @@ | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 66 |  		{
 | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 67 | int following = charBreaker.following(offset - | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 68 | index0Offset); | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 69 | - if (following == BreakIterator.DONE) | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 70 | + if (following == BreakIterator.DONE || (Runtime.version().feature() >= 20 && following == offset - index0Offset)) | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 71 |  			{
 | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 72 | // This means a end of line. Then it is | 
| 
b6bca0666c38
rebuild jedit with minimal patch for jdk-21, following SVN 25690;
 wenzelm parents: 
73658diff
changeset | 73 | // safe to assume 1 code unit is a character. | 
| 73658 | 74 | diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java | 
| 75 | --- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2020-09-03 05:31:03.000000000 +0200 | |
| 76 | +++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java 2021-05-10 18:20:57.418571547 +0200 | |
| 77 | @@ -115,6 +115,8 @@ | |
| 78 | case '⦄': if (direction != null) direction[0] = false; return '⦃'; | |
| 79 | case '⟪': if (direction != null) direction[0] = true; return '⟫'; | |
| 80 | case '⟫': if (direction != null) direction[0] = false; return '⟪'; | |
| 81 | + case '⦉': if (direction != null) direction[0] = true; return '⦊'; | |
| 82 | + case '⦊': if (direction != null) direction[0] = false; return '⦉'; | |
| 83 | default: return '\0'; | |
| 84 | } | |
| 85 | } //}}} | |
| 73653 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 86 | diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java | 
| 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 87 | --- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200 | 
| 
d9823224fcfe
build auxiliary jEdit component in Isabelle/Scala;
 wenzelm parents: 
72247diff
changeset | 88 | +++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java 2021-05-10 11:02:05.820257742 +0200 | 
| 71932 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 89 | @@ -344,8 +344,28 @@ | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 90 | } | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 91 | } | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 92 | |
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 93 | - return styles; | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 94 | + styles[0] = | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 95 | +			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
 | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 96 | + null, new Font(family, 0, size)); | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 97 | + return _styleExtender.extendStyles(styles); | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 98 | } //}}} | 
| 
65fd0f032a75
updated to jedit-5.6pre1 (repository version 25349);
 wenzelm parents: 
69838diff
changeset | 99 | |
| 48786 | 100 | + /** | 
| 101 | + * Extended styles derived from the user-specified style array. | |
| 102 | + */ | |
| 103 | + | |
| 104 | + public static class StyleExtender | |
| 105 | +	{
 | |
| 106 | + public SyntaxStyle[] extendStyles(SyntaxStyle[] styles) | |
| 107 | +		{
 | |
| 108 | + return styles; | |
| 109 | + } | |
| 110 | + } | |
| 111 | + volatile private static StyleExtender _styleExtender = new StyleExtender(); | |
| 112 | + public static void setStyleExtender(StyleExtender ext) | |
| 113 | +	{
 | |
| 114 | + _styleExtender = ext; | |
| 115 | + } | |
| 116 | + | |
| 117 |  	private SyntaxUtilities(){}
 | |
| 118 | } |