src/Tools/jEdit/patches/extended_styles_brackets
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 82181 a0d1d772ccab
child 82625 0fa6759948bc
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
     1
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
     2
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2024-08-03 19:53:18.000000000 +0200
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
     3
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2024-10-29 11:50:54.066016546 +0100
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
     4
@@ -332,9 +332,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
72247
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset
    16
@@ -584,8 +584,8 @@
c06260b7152c update to official jedit-5.6.0;
wenzelm
parents: 71932
diff changeset
    17
 	// this is either style.getBackgroundColor() or
48786
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;
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    20
-	private char[] chars;
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    21
-	private String str;
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    22
+	public char[] chars;
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    23
+	public String str;
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    24
 	private GlyphData glyphData;
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    25
 	//}}}
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50305
diff changeset
    26
 
80156
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    27
@@ -926,6 +926,11 @@
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    28
 		}
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    29
 
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    30
 		@Override
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    31
+		public GlyphData computeIfAbsent(GlyphKey key, java.util.function.Function<? super GlyphKey, ? extends GlyphData> f) {
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    32
+			synchronized (this) { return super.computeIfAbsent(key, f); }
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    33
+		}
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    34
+
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    35
+		@Override
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    36
 		protected boolean removeEldestEntry(Map.Entry<GlyphKey, GlyphData> eldest)
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    37
 		{
70d69b081561 more robust: avoid spurious ConcurrentModificationException;
wenzelm
parents: 79012
diff changeset
    38
 			return size() > capacity;
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    39
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    40
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2024-08-03 19:53:18.000000000 +0200
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    41
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2024-10-29 11:50:54.066016546 +0100
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    42
@@ -919,6 +919,11 @@
61511
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    43
 		return chunkCache.getLineInfo(screenLine).physicalLine;
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    44
 	} //}}}
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    45
 
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    46
+        public Chunk getChunksOfScreenLine(int screenLine)
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    47
+        {
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    48
+                return chunkCache.getLineInfo(screenLine).chunks;
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    49
+        }
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    50
+
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    51
 	//{{{ getScreenLineOfOffset() method
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    52
 	/**
d40f906bb13f updated to jedit-5.3.0 and SideKick 1.8;
wenzelm
parents: 59571
diff changeset
    53
 	 * Returns the screen (wrapped) line containing the specified offset.
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    54
@@ -1627,8 +1632,8 @@
73658
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    55
 		}
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    56
 
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    57
 		// Scan backwards, trying to find a bracket
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    58
-		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    59
-		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    60
+		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉";
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    61
+		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊";
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    62
 		int count = 1;
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    63
 		char openBracket = '\0';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    64
 		char closeBracket = '\0';
82181
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    65
@@ -4983,6 +4988,7 @@
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    66
 	final Point offsetXY;
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    67
 
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    68
 	boolean lastLinePartial;
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    69
+	public boolean isLastLinePartial() { return lastLinePartial; }
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    70
 
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    71
 	boolean blink;
a0d1d772ccab more robust jEdit Emacs Macros, based on patch #642 "bundled Emacs Macros are broken" (still open in jedit-5.7.0);
wenzelm
parents: 81297
diff changeset
    72
 	//}}}
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    73
diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    74
--- jedit5.7.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2024-08-03 19:53:20.000000000 +0200
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    75
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java	2024-10-29 11:50:54.066016546 +0100
73658
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    76
@@ -115,6 +115,8 @@
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    77
 		case '⦄': if (direction != null) direction[0] = false; return '⦃';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    78
 		case '⟪': if (direction != null) direction[0] = true;  return '⟫';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    79
 		case '⟫': if (direction != null) direction[0] = false; return '⟪';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    80
+		case '⦉': if (direction != null) direction[0] = true;  return '⦊';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    81
+		case '⦊': if (direction != null) direction[0] = false; return '⦉';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    82
 		default:  return '\0';
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    83
 		}
f6b453449cc6 more brackets;
wenzelm
parents: 73653
diff changeset
    84
 	} //}}}
81297
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    85
diff -ru jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    86
--- jedit5.7.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2024-08-03 19:53:21.000000000 +0200
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    87
+++ jedit5.7.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2024-10-29 11:50:54.066016546 +0100
07f64697408e update to jedit5.7.0;
wenzelm
parents: 80156
diff changeset
    88
@@ -357,8 +357,28 @@
71932
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    89
 			}
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    90
 		}
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    91
 
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    92
-		return styles;
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    93
+		styles[0] =
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    94
+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    95
+				null, new Font(family, 0, size));
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    96
+		return _styleExtender.extendStyles(styles);
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    97
 	} //}}}
65fd0f032a75 updated to jedit-5.6pre1 (repository version 25349);
wenzelm
parents: 69838
diff changeset
    98
 
48786
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
    99
+	/**
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   100
+	 * Extended styles derived from the user-specified style array.
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   101
+	 */
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   102
+
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   103
+	public static class StyleExtender
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   104
+	{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   105
+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   106
+		{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   107
+			return styles;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   108
+		}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   109
+	}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   110
+	volatile private static StyleExtender _styleExtender = new StyleExtender();
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   111
+	public static void setStyleExtender(StyleExtender ext)
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   112
+	{
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   113
+		_styleExtender = ext;
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   114
+	}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   115
+
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   116
 	private SyntaxUtilities(){}
2b08d10a2f75 updated to jedit-4.5.2 (still unchanged);
wenzelm
parents:
diff changeset
   117
 }