src/Tools/jEdit/patches/extended_styles
author wenzelm
Sun Feb 24 12:49:32 2019 +0100 (2 months ago ago)
changeset 70019 4419d4d675c3
parent 67993 752a4e6d760c
permissions -rw-r--r--
formal update of patches -- no change of content;
     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
     2 --- 5.5.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2018-04-09 01:57:24.000000000 +0200
     3 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java	2019-02-24 12:32:09.336643045 +0100
     4 @@ -322,9 +322,9 @@
     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
    16 @@ -572,7 +572,7 @@
    17  	// this is either style.getBackgroundColor() or
    18  	// styles[defaultID].getBackgroundColor()
    19  	private Color background;
    20 -	private String str;
    21 +	public String str;
    22  	private GlyphVector[] glyphs;
    23  	//}}}
    24  
    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
    26 --- 5.5.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2018-04-09 01:58:01.000000000 +0200
    27 +++ 5.5.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java	2019-02-24 12:20:10.550459878 +0100
    28 @@ -917,6 +917,11 @@
    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.
    40 diff -ru 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
    41 --- 5.5.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2018-04-09 01:58:37.000000000 +0200
    42 +++ 5.5.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java	2019-02-24 12:20:10.550459878 +0100
    43 @@ -200,7 +200,24 @@
    44  	{
    45  		return loadStyles(family,size,true);
    46  	}
    47 -	
    48 +
    49 +	/**
    50 +	 * Extended styles derived from the user-specified style array.
    51 +	 */
    52 +
    53 +	public static class StyleExtender
    54 +	{
    55 +		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
    56 +		{
    57 +			return styles;
    58 +		}
    59 +	}
    60 +	volatile private static StyleExtender _styleExtender = new StyleExtender();
    61 +	public static void setStyleExtender(StyleExtender ext)
    62 +	{
    63 +		_styleExtender = ext;
    64 +	}
    65 +
    66  	/**
    67  	 * Loads the syntax styles from the properties, giving them the specified
    68  	 * base font family and size.
    69 @@ -230,9 +247,11 @@
    70  				Log.log(Log.ERROR,StandardUtilities.class,e);
    71  			}
    72  		}
    73 -
    74 -		return styles;
    75 +		styles[0] =
    76 +			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
    77 +				null, new Font(family, 0, size));
    78 +		return _styleExtender.extendStyles(styles);
    79  	} //}}}
    80 -	
    81 +
    82  	private SyntaxUtilities(){}
    83  }