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: Scala

Original von: Isabelle©

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.18 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff