products/sources/formale Sprachen/Isabelle/Tools/jEdit/patches/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: extended_styles   Sprache: Unknown

diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/syntax/Chunk.java 2020-09-08 20:13:23.565140195 +0200
@@ -332,9 +332,9 @@
  //{{{ Package private members
 
  //{{{ Instance variables
- SyntaxStyle style;
+ public SyntaxStyle style;
  // set up after init()
- float width;
+ public float width;
  //}}}
 
  //{{{ Chunk constructor
@@ -584,8 +584,8 @@
  // this is either style.getBackgroundColor() or
  // styles[defaultID].getBackgroundColor()
  private Color background;
- private char[] chars;
- private String str;
+ public char[] chars;
+ public String str;
  private GlyphData glyphData;
  //}}}
 
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
--- 5.6.0/jEdit-orig/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-03 05:31:01.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2020-09-08 20:13:23.569140077 +0200
@@ -914,6 +914,11 @@
   return chunkCache.getLineInfo(screenLine).physicalLine;
  } //}}}
 
+        public Chunk getChunksOfScreenLine(int screenLine)
+        {
+                return chunkCache.getLineInfo(screenLine).chunks;
+        }
+
  //{{{ getScreenLineOfOffset() method
  /**
   * Returns the screen (wrapped) line containing the specified offset.
diff -ru 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
--- 5.6.0/jEdit-orig/org/gjt/sp/util/SyntaxUtilities.java 2020-09-03 05:31:09.000000000 +0200
+++ 5.6.0/jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java 2020-09-08 20:13:23.569140077 +0200
@@ -344,8 +344,28 @@
    }
   }
 
-  return styles;
+  styles[0] =
+   new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
+    null, new Font(family, 0, size));
+  return _styleExtender.extendStyles(styles);
  } //}}}
 
+ /**
+  * Extended styles derived from the user-specified style array.
+  */
+
+ public static class StyleExtender
+ {
+  public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
+  {
+   return styles;
+  }
+ }
+ volatile private static StyleExtender _styleExtender = new StyleExtender();
+ public static void setStyleExtender(StyleExtender ext)
+ {
+  _styleExtender = ext;
+ }
+
  private SyntaxUtilities(){}
 }

[ Dauer der Verarbeitung: 0.17 Sekunden  (vorverarbeitet)  ]